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.
|Electronic Notes in Theoretical Computer Science
|Published - 5 Jul 2005
|Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2005) -
Duration: 16 Jul 2005 → 16 Jul 2005