| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 10329440 | Electronic Notes in Theoretical Computer Science | 2005 | 19 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Alexey Gotsman, Fabio Massacci, Marco Pistore,