Affordable Access

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

Authors
  • Chevalier, Yannick
  • Compagna, Luca
  • Cuellar, Jorge
  • Hankes Drielsma, Paul
  • Mantovani, Jacopo
  • Moedersheim, Sebastian
  • Vigneron, Laurent
Publication Date
Jan 01, 2004
Source
HAL-INRIA
Keywords
Language
English
License
Unknown
External links

Abstract

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.

Report this publication

Statistics

Seen <100 times