A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols
Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Jacopo Mantovani, Sebastian Moedersheim, Laurent Vigneron · 2004
Abstract. 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. 1.