The AVISPA Tool for the automated validation of internet security protocols and applications

Alessandro Armando; David Basin; Yohan Boichut; Yannick Chevalier; Luca Compagna; Jorge Cuellar; Paul Hankes Drielsma; Pierre-Cyrille Héam; Olga Kouchnarenko; Jacopo Mantovani; Sebastian Mödersheim; David Von Oheimb; Michaël Rusinowitch; Judson Santos Santiago; Luca Vigano; Mathieu Turuani; Laurent Vigneron

inria-00000408, version 1

The AVISPA Tool for the automated validation of internet security protocols and applications

Alessandro Armando ¹, David Basin ², Yohan Boichut ³, Yannick Chevalier ³, Luca Compagna ¹, Jorge Cuellar ⁴, Paul Hankes Drielsma ², Pierre-Cyrille Héam ³, Olga Kouchnarenko ³, Jacopo Mantovani ¹, Sebastian Mödersheim ², David Von Oheimb ⁴, Michaël Rusinowitch ³, Judson Santos Santiago ³, Luca Vigano ², Mathieu Turuani ³, Laurent Vigneron () ³

17th International Conference on Computer Aided Verification - CAV 2005 3576 (2005) 281-285

Résumé : AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.

1 : Department of informatics, systems and telecommunications (DIST)
Università degli studi di Genova
2 : Eldgenössische Technische Hochschule Zürich (ETH Zürich)
ETH Zurich
3 : CASSIS (INRIA Lorraine - LORIA / LIFC)
INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
4 : Siemens AG (SIEMENS)
Siemens

inria-00000408, version 1
http://hal.inria.fr/inria-00000408
oai:hal.inria.fr:inria-00000408
Contributeur : Laurent Vigneron <>
Soumis le : Jeudi 6 Octobre 2005, 18:36:02
Dernière modification le : Jeudi 8 Octobre 2009, 15:59:51

Voir la fiche détaillée

Documents associés

PS :

PDF :

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Communications avec actes</head>
<biblStruct type="inproceedings" xml:id="inria-00000408"><analytic>
<author><persName><forename>Alessandro</forename><surname>Armando</surname></persName>
<affiliation>
<orgName type="laboratory">DIST</orgName>
<orgName type="team">Department of informatics, systems and telecommunications</orgName>
<country>IT</country>
<orgName type="institution">Università degli studi di Genova</orgName>
</affiliation>
</author>
<author><persName><forename>David</forename><surname>Basin</surname></persName>
<affiliation>
<orgName type="laboratory">ETH Zürich</orgName>
<orgName type="team">Eldgenössische Technische Hochschule Zürich</orgName>
<country>CH</country>
<orgName type="institution">ETH Zurich</orgName>
</affiliation>
</author>
<author><persName><forename>Yohan</forename><surname>Boichut</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Yannick</forename><surname>Chevalier</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Luca</forename><surname>Compagna</surname></persName>
<affiliation>
<orgName type="laboratory">DIST</orgName>
<orgName type="team">Department of informatics, systems and telecommunications</orgName>
<country>IT</country>
<orgName type="institution">Università degli studi di Genova</orgName>
</affiliation>
</author>
<author><persName><forename>Jorge</forename><surname>Cuellar</surname></persName>
<affiliation>
<orgName type="laboratory">SIEMENS</orgName>
<orgName type="team">Siemens AG</orgName>
<country>DE</country>
<orgName type="institution">Siemens</orgName>
</affiliation>
</author>
<author><persName><forename>Paul</forename><surname>Hankes Drielsma</surname></persName>
<affiliation>
<orgName type="laboratory">ETH Zürich</orgName>
<orgName type="team">Eldgenössische Technische Hochschule Zürich</orgName>
<country>CH</country>
<orgName type="institution">ETH Zurich</orgName>
</affiliation>
</author>
<author><persName><forename>Pierre-Cyrille</forename><surname>Héam</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Olga</forename><surname>Kouchnarenko</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Jacopo</forename><surname>Mantovani</surname></persName>
<affiliation>
<orgName type="laboratory">DIST</orgName>
<orgName type="team">Department of informatics, systems and telecommunications</orgName>
<country>IT</country>
<orgName type="institution">Università degli studi di Genova</orgName>
</affiliation>
</author>
<author><persName><forename>Sebastian</forename><surname>Mödersheim</surname></persName>
<affiliation>
<orgName type="laboratory">ETH Zürich</orgName>
<orgName type="team">Eldgenössische Technische Hochschule Zürich</orgName>
<country>CH</country>
<orgName type="institution">ETH Zurich</orgName>
</affiliation>
</author>
<author><persName><forename>David</forename><surname>Von Oheimb</surname></persName>
<affiliation>
<orgName type="laboratory">SIEMENS</orgName>
<orgName type="team">Siemens AG</orgName>
<country>DE</country>
<orgName type="institution">Siemens</orgName>
</affiliation>
</author>
<author><persName><forename>Michaël</forename><surname>Rusinowitch</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Judson</forename><surname>Santos Santiago</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Luca</forename><surname>Vigano</surname></persName>
<affiliation>
<orgName type="laboratory">ETH Zürich</orgName>
<orgName type="team">Eldgenössische Technische Hochschule Zürich</orgName>
<country>CH</country>
<orgName type="institution">ETH Zurich</orgName>
</affiliation>
</author>
<author><persName><forename>Mathieu</forename><surname>Turuani</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Laurent</forename><surname>Vigneron</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">The AVISPA Tool for the automated validation of internet security protocols and applications</title></analytic><monogr><meeting>17th International Conference on Computer Aided Verification - CAV 2005</meeting><imprint><publisher>Springer</publisher><pubPlace><settlement>Edinburgh, Scotland/UK</settlement><country>France</country></pubPlace><biblScope type="publicationDate">2005-07-00</biblScope><biblScope type="vol">3576</biblScope><biblScope type="pp">281-285</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00000408</idno><idno type="HALFile">http://hal.inria.fr/inria-00000408/PDF/avispa-cav.pdf</idno></biblStruct>
</listBibl>
</listBibl>