[TYPES/announce] The AVISPA Tool - v1.1
Laurent.Vigneron@loria.fr
Laurent.Vigneron at loria.fr
Fri Jun 30 19:17:55 EDT 2006
[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
http://www.avispa-project.org
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).
========
OVERVIEW
========
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
====
NEWS
====
* 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
"hash_func".
- 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
handled.
- 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
theory.
* 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.
========
PARTNERS
========
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',
France
* Eidgenoessische Technische Hochschule Zuerich (ETHZ),
Information Security Group, Department of Computer Science,
Zuerich, Switzerland
* Siemens Aktiengesellschaft, Munich, Germany
================
GETTING IN TOUCH
================
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
<avispa-users-join-project.org>
New releases and other important events for AVISPA will be also
announced on this list.
--
The AVISPA Team
http://www.avispa-project.org
More information about the Types-announce
mailing list