Towards an independent semantics and verification technology for the HLPSL specification language

A. Gotsman; F. Massacci; M. Pistore

doi:10.1016/j.entcs.2005.06.004

Towards an independent semantics and verification technology for the HLPSL specification language

A. Gotsman, F. Massacci, M. Pistore

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

We present an algorithm for the translation of security protocol specifications in the HLPSL language developed in the framework of the AVISPA project to a dialect of the applied pi calculus. This algorithm provides us with two interesting scientific contributions: at first, it provides an independent semantics of the HLPSL specification language and, second, makes it possible to verify protocols specified in HLPSL with the applied pi calculus-based ProVerif tool. Our technique has been implemented and tested on various security protocols. The translation can handle a large part of the protocols modelled in HLPSL. © 2005 Elsevier B.V. All rights reserved.

Original language	English
Pages (from-to)	59-77
Journal	Electronic Notes in Theoretical Computer Science
Volume	135
Issue number	1
DOIs	https://doi.org/10.1016/j.entcs.2005.06.004
Publication status	Published - 5 Jul 2005
Externally published	Yes
Event	Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2005) - Duration: 16 Jul 2005 → 16 Jul 2005

Access to Document

10.1016/j.entcs.2005.06.004

Persistent URL (handle)

Persistent link

Cite this

@article{b7c69fce531c4f05a6fcbefc9eddbf1e,

title = "Towards an independent semantics and verification technology for the HLPSL specification language",

abstract = "We present an algorithm for the translation of security protocol specifications in the HLPSL language developed in the framework of the AVISPA project to a dialect of the applied pi calculus. This algorithm provides us with two interesting scientific contributions: at first, it provides an independent semantics of the HLPSL specification language and, second, makes it possible to verify protocols specified in HLPSL with the applied pi calculus-based ProVerif tool. Our technique has been implemented and tested on various security protocols. The translation can handle a large part of the protocols modelled in HLPSL. {\textcopyright} 2005 Elsevier B.V. All rights reserved.",

author = "A. Gotsman and F. Massacci and M. Pistore",

year = "2005",

month = jul,

day = "5",

doi = "10.1016/j.entcs.2005.06.004",

language = "English",

volume = "135",

pages = "59--77",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "1",

note = "Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2005) ; Conference date: 16-07-2005 Through 16-07-2005",

}

TY - JOUR

T1 - Towards an independent semantics and verification technology for the HLPSL specification language

AU - Gotsman, A.

AU - Massacci, F.

AU - Pistore, M.

PY - 2005/7/5

Y1 - 2005/7/5

N2 - We present an algorithm for the translation of security protocol specifications in the HLPSL language developed in the framework of the AVISPA project to a dialect of the applied pi calculus. This algorithm provides us with two interesting scientific contributions: at first, it provides an independent semantics of the HLPSL specification language and, second, makes it possible to verify protocols specified in HLPSL with the applied pi calculus-based ProVerif tool. Our technique has been implemented and tested on various security protocols. The translation can handle a large part of the protocols modelled in HLPSL. © 2005 Elsevier B.V. All rights reserved.

AB - We present an algorithm for the translation of security protocol specifications in the HLPSL language developed in the framework of the AVISPA project to a dialect of the applied pi calculus. This algorithm provides us with two interesting scientific contributions: at first, it provides an independent semantics of the HLPSL specification language and, second, makes it possible to verify protocols specified in HLPSL with the applied pi calculus-based ProVerif tool. Our technique has been implemented and tested on various security protocols. The translation can handle a large part of the protocols modelled in HLPSL. © 2005 Elsevier B.V. All rights reserved.

U2 - 10.1016/j.entcs.2005.06.004

DO - 10.1016/j.entcs.2005.06.004

M3 - Article

SN - 1571-0661

VL - 135

SP - 59

EP - 77

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 1

T2 - Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2005)

Y2 - 16 July 2005 through 16 July 2005

ER -

Towards an independent semantics and verification technology for the HLPSL specification language

Abstract

Access to Document

Persistent URL (handle)

Fingerprint

Cite this