The AVISPA tool
NEW!
The AVISPA tool version 1.1 has been released (June 30, 2006) and
can be downloaded here.
SPAN, the Security Protocol ANimator for AVISPA
NEW!
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 Tool Web Interface
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
download and install
on a local machine the code of the web-based interface.
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.
-
The On-the-fly Model-Checker (OFMC) performs protocol
falsification and bounded verification by exploring the transition
system described by an IF specification in a demand-driven way. OFMC
implements a number of correct and complete symbolic techniques. It
supports the specification of algebraic properties of cryptographic
operators, and typed and untyped protocol models.
-
The Constraint-Logic-based Attack Searcher (CL-AtSe)
applies constraint solving with some powerful simplification
heuristics and redundancy elimination techniques. CL-AtSe is built
in a modular way and is open to extensions for handling algebraic
properties of cryptographic operators. It supports type-flaw
detection and handles associativity of message concatenation.
-
The SAT-based Model-Checker (SATMC) builds a
propositional formula encoding a bounded unrolling of the transition
relation specified by the IF, the initial state and the set of
states representing a violation of the security properties. The
propositional formula is then fed to a state-of-the-art SAT solver
and any model found is translated back into an attack.
-
The Tree Automata based on Automatic Approximations for
the Analysis of Security Protocols (TA4SP) back-end approximates
the intruder knowledge by using regular tree languages and
rewriting. For secrecy properties, TA4SP can show whether a
protocol is flawed (by under-approximation) or whether it is safe
for any number of sessions (by over-approximation).