[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] The AVISPA Tool - v1.1

[We apologize if you received multiple copies of this message]

             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 . 1

                            (June 30, 2006)

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


The AVISPA Tool v1.1 includes several bug fixes and extends the
previous versions of the AVISPA Tool with several new features (see
the NEWS section below).


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, 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.

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 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


* All known bugs have been fixed.

* All back-ends have been optimised for improved performance.

* The translator from HLPSL to IF has been improved, with only minor
  changes in the syntax:

  - The HLPSL type "function" being too ambiguous, it has been renamed

  - More semantic tests are done for detecting incomplete goal
    specifications or missing new() assignments.

  - The handling of sets has been simplified in the translator.

  - Predefined constant functions, like xor and exp, are better

  - Warning and error messages are more precise.

* OFMC, CL-AtSe, and SATMC support user-defined (non temporal)
  security goals.

* OFMC now supports reasoning modulo a user-specified algebraic

* CL-Atse has improved in many ways:

  - Algebraic properties : CL-Atse now supports complete analysis of
    cryptographic protocols modulo the xor, including all the intruder
    deduction rules for that operator.  CL-Atse also implements
    complete analysis modulo the exponential except for the rule g^1 =
    g (i.e. exponentials are tagged).  Also, some improvements on the
    code for algebraic properties (speed, bug correction, etc.) have
    been added.

  - The protocol optimisation module now allows CL-Atse to perform
    advanced optimisations of the protocol specification before the
    analysis, and may greatly reduce the analysis time.  Now, CL-Atse
    can statically decide the origin of certain messages and reduce
    the non-determinism of the analysis accordingly.

  - User interaction (output presentation, options, etc..) improved.

* The AVISPA XEmacs mode has been improved and it is now a powerful
 environment for writing protocol specifications and analysing them.

* A new contribution has been added: hlpsldoc.  It contains script
  files that automatically generate either a LaTeX file or a HTML file
  from a HLPSL specification.  It has been used to generate the online
  AVISPA library.


The following research groups have contributed to the development of
the AVISPA Tool:

 * 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 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


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