Abstract:

A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols

Yannick Chevalier and Luca Compagna and Jorge Cuellar and Paul Hankes Drielsma and Jacopo Mantovani and Sebastian Mödersheim and Laurent Vigneron


This paper presents HLPSL, a high-level protocol specification language for the modelling of security-sensitive 
protocols. This language has a formal semantics based on Lamport s Temporal Logic of Actions. HLPSL is 
modular and allows for the specification of control flow patterns, data-structures, alternative intruder models, and
 complex security properties. It is sufficiently highlevel to be accessible to protocol engineers (themselves not 
necessarily formal methods experts), yet easily translatable into a lower-level term-rewriting based language 
well-suited to model-checking tools. The accommodation of these contrasting features makes HLPSL able to 
easily specify modern, industrial-scale protocols on which existing specification languages only partially succeed.