A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols
Résumé
This paper presents HLPSL, a high level protocol specification language for the modelling of security-sensitive cryptographic protocols. This language enjoys 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 high-level 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.