The High-Level Protocol Specification Language HLPSL developed in the EU project AVISPA 论文

摘要

The just recently finished EU project AVISPA, Automated Validation of Internet Security Protocols and Applications, has aimed at developing a push-button, industrial-strength technology for the analysis of large-scale Internet security-sensitive protocols and applications. In this short industrial contribution paper, after giving a very brief overview of the AVISPA project, we introduce HLPSL, the High-Level Protocol Specification Language developed and used within the project to model security protocols and to specify their desired properties. 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 suciently 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 suited to model-checking tools.