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