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.
Towards an Independent Semantics and Verification Technology for the HLPSL Specification Language
Massacci, Fabio;Pistore, Marco;
2005-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
