The AVISPA tool

The AVISPA tool version 1.1 has been released (June 30, 2006) and can be downloaded here.

SPAN, the Security Protocol ANimator for AVISPA

SPAN is designed to help protocol developers in writing HLPSL specifications. From an HLPSL specification SPAN helps in interactively buiding Message Sequence Charts (MSC) of the protocol execution. Since SPAN implements an active intruder, it can also be used to interactively find and build attacks over protocols.

Download SPAN

The AVISPA Docker Tool Chain

NEW!

A docker-based tool chain for running the AVISPA tool directly in your environment is also available. You can find a unix shell script here. To run it open a terminal and type

 $> ./ochestrator.sh 

Please notice that the docker tool chain is still under development and testing. Please report bugs and issues.

The AVISPA Tool Web Interface (Deprecated)

A web-based interface for running the AVISPA tool directly in your browser is also available here.

Please notice that the web interface is for demonstration purposes only. If you plan to make an intensive use of the AVISPA web interface (e.g. for a practical in a course), please contact us.

More details on the AVISPA components:

The HLPS2IF translator

The HLPSL is an expressive, modular, role-based, formal language that allows for the specification of control flow patterns, data-structures, alternative intruder models, complex security properties, as well as different cryptographic primitives and their algebraic properties. These features make HLPSL well suited for specifying modern, industrial-scale protocols. Moreover, the HLPSL enjoys both a declarative semantics based on a fragment of the Temporal Logic of Actions and an operational semantics based on a translation into the rewrite-based formalism Intermediate Format IF.

HLPSL2IF automatically translates HLPSL specifications into equivalent IF specifications which are in turn fed to the back-ends.

HLPSL2IF is part of the AVISPA Tool v1.0 and is written in OCAML, a freely-distributed object-oriented version of ML which you can obtain at http://www.ocaml.org.

The AVISPA backends

AVISPA employs four tools to tackle validation of security protocols.