[TYPES] The AVISPA Tool v.1.0 - Official release
AVISPA
avispa at carroll.ai.dist.unige.it
Tue Jun 14 21:33:38 EDT 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:
http://www.avispa-project.org/download.html
For more information about the AVISPA Project, you may look at
http://www.avispa-project.org.
The announcement of this release of the tool is enclosed below.
The AVISPA Team
--------------------------------------------------------------------
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
http://www.avispa-project.org
===========================
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
========
PARTNERS
========
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',
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 <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.
--
The AVISPA Team
http://www.avispa-project.org
--------------------------------------------------------------------
More information about the Types-list
mailing list