[loginf] The AVISPA Tool v.1.0 - Official release

AVISPA avispa at carroll.ai.dist.unige.it
Tue Jun 14 20:33:25 CEST 2005

Dear colleague,

we are happy to announce the availability of the AVISPA Tool v1.0 for
the Automatic Validation of Internet Security-sensitive Protocols and
Applications. It is downloadable by following the link below:


For more information about the AVISPA Project, you may look at

The announcement of this release of the tool is enclosed below.



             XXX   X     X  XXXXX   XXXXX  XXXXXX    XXX                                  
            X   X  X     X    X    X     X X     X  X   X                                 
           X     X X     X    X    X       X     X X     X                                
           X     X  X   X     X    X       X     X X     X                                
           XXXXXXX  X   X     X     XXXXX  XXXXXX  XXXXXXX                                
           X     X   X X      X          X X       X     X                                
           X     X   X X      X          X X       X     X                                
           X     X    X       X    X     X X       X     X                                
           X     X    X     XXXXX   XXXXX  X       X     X                                

                     V E R S I O N    1 . 0

                            (June 14, 2005)

We are happy to announce the availability of the AVISPA Tool v1.0, a
push-button tool for the Automatic Validation of Internet
Security-sensitive Protocols and Applications.  The AVISPA Tool v1.0
is available at


Overview of the AVISPA Tool

The AVISPA Tool is a push-button tool for the automated validation of
Internet security-sensitive protocols and applications.  It provides a
modular and expressive formal language (called HLPSL) for specifying
protocols and their security properties, and integrates different
back-ends that implement a variety of state-of-the-art automatic
analysis techniques ranging from protocol falsification (by finding an
attack on the input protocol) to abstraction-based verification
methods for both finite and infinite numbers of sessions.

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.
The AVISPA Tool automatically translates HLPSL specifications into
equivalent IF specifications which are in turn fed to the back-ends.

Currently the following back-ends are integrated in the AVISPA Tool:

* 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 TA4SP (Tree Automata based on Automatic Approximations for the
  Analysis of Security Protocols) 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).

In order to demonstrate the effectiveness of the AVISPA Tool on a
large collection of practically relevant, industrial protocols, we
have selected a substantial set of security problems associated with
protocols that have recently been or are currently being standardized
by organizations like the Internet Engineering Task Force IETF.  We
have then formalized in HLPSL a large subset of these protocols, and
the result of this specification effort is the AVISPA Library
(publicly available at the AVISPA web-page), which at present
comprises 112 security problems derived from 33 protocols.

Further details on the AVISPA Tool v1.0 and on the AVISPA project can
be found in the paper:

A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna,
J. Cuellar, P. Hankes Drielsma, P.C. Heam, O. Kouchnarenko,
J. Mantovani, S. Moedersheim, D. von Oheimb, M. Rusinowitch,
J. Santiago, M. Turuani, L. Vigano`, L. Vigneron.  "The AVISPA Tool
for the Automated Validation of Internet Security Protocols and
Applications."  In Proc. CAV'05, LNCS. Springer Verlag, 2005,
Available at the URL http://www.avispa-project.org/avispa-cav05.ps


The following research groups have contribute to the development of
the AVISPA Tool v1.0:

 * Artificial Intelligence Laboratory,
   Dipartimento di Informatica, Sistemistica e Telematica (DIST),
   University of Genova, Italy

 * Laboratoire Lorrain de Recherche en Informatique et ses Applications 
   (LORIA UMR 7503) with partners INRIA, CNRS, Universite' Henri Poincare' (UHP)
   Université Nancy 2  AND  
   Laboratoire d'Informatique de l'Universite' de Franche-Comte',

 * Eidgenoessische Technische Hochschule Zuerich (ETHZ),
   Information Security Group, Department of Computer Science,
   Zuerich, Switzerland

 * Siemens Aktiengesellschaft, Munich, Germany


The home page of the AVISPA project is <http://www.avispa-project.org>.

A mailing list <avispa-users at avispa-project.org> for general
questions, bugs and bug fixes, possible extensions, and user requests
on the AVISPA Tool is available.  To register please send an empty
message to

              <avispa-users-join at avispa-project.org>

New releases and other important events for AVISPA will be also
announced on this list.


More information about the loginf mailing list