HLPSL

The High Level Protocol Specification Language (HLPSL) is an expressive language for
modelling communication and security protocols. HLPSL draws its semantic roots from
Lamport’s Temporal Logic of Actions. TLA is an elegant and powerful language
which lends itself well to specifying concurrent systems. Syntactically, however, specifying protocols in a raw logic can be a daunting task. Moreover, the domain of protocol analysis calls for several syntactic constructs (such as message structure) and semantic concepts (like the notion of an intruder) that are problem-independent and arise in every model. Ideally, it would be convenient to model protocols in a language which offers such commonalities built-in. The development of HLPSL was thus undertaken with the following design objectives:
 •   It must provide a convenient, human readable, and easy to use language yet be
 powerful enough to support the specification of modern Internet protocols. To this
 end, HLPSL has been defined in such a way as to closely resemble a language for
 defining guarded transitions within a state-transition system and is equipped with
 constructs which allow the modular specification of protocols.
• It must enjoy a formal semantics. To this end, HLPSL has been based on Lamport’s
 TLA and its semantics is given by a translation to a subset of TLA.
• It must be amenable to automated formal analysis. This is achieved by a translation
  of HLPSL into the Intermediate Format (IF).

Architecture:

HLPSL is the language through which end users and protocol modellers make use of the

AVISPA (Automated Validation of Internet Security Protocols and Applications) tool-set. As such, it is designed to be accessible: it should be easy for human users to both read and write HLPSL specifications. To this end, HLPSL provides a high level of abstraction and has many features that are common to most protocol specifications – such as intruder models and encryption primitives – built in. In contrast, the Intermediate Format (IF) – the language into which HLPSL specifications are translated – is a lower-level language at an accordingly lower abstraction level.

References: AVISPA IST-2001-39252