Download HLPSL Tutorial - The AVISPA Project

CONTENTS
2
Introduction
The AVISPA Tool provides a suite of applications for building and analysing formal models of
security protocols. Protocol models are written in the High Level Protocol Specification Language,
or HLPSL [3, 9]. The aim of this tutorial is to provide some advice on constructing protocol models
in HLPSL.
In addition to this tutorial, the AVISPA Package User Manual [5] is another useful resource
for beginners to HLPSL. Please refer to this manual if you require further information on HLPSL
or any of the tools discussed throughout this tutorial.
Organisation of this tutorial: Section 1 contains a very basic introduction to what HLPSL looks
like and how it is used.
Section 2 contains four introductory examples that illustrate modelling with HLPSL. In discussing the examples, we attempt to show both correct solutions and possible pitfalls that modellers should be aware of.
Section 3 contains a number of tips useful for writing or reading HLPSL specifications.
Finally, Section 4 provides a list of questions and answers about HLPSL,
followed by an appendix containing a list of HLPSL keywords and symbols.
AVISPA
HLPSL Tutorial