The AVISS Security Protocol Analysis Tool

Alessandro Armando; David Basin; Mehdi Bouallagui; Yannick Chevalier; Luca Compagna; Sebastian Moedersheim; Michaël Rusinowitch; Mathieu Turuani; Luca Vigano; Laurent Vigneron

inria-00100915, version 1

The AVISS Security Protocol Analysis Tool

Alessandro Armando^a, David Basin^b, Mehdi Bouallagui^c^, 1, Yannick Chevalier^d^, 1, Luca Compagna^a, Sebastian Moedersheim^b, Michaël Rusinowitch^c^, 1, Mathieu Turuani^e^, 1, Luca Vigano^b, Laurent Vigneron ()^e^, 1

14th International Conference on Computer Aided Verification - CAV'2002 2404 (2002) 349-353

Résumé : We introduce AVISS, a tool for security protocol analysis that supports the integration of back-ends implementing different search techniques, allowing for their systematic and quandtitative comparison and paving the way to their effective interaction. As a significant example, we have implemented three back-ends, and used the AVISS tool to analyse and find flaws in 36 protocols, including 31 problems in the Clark-Jacob's protocol library and a previously unreported flaw in the Denning-Sacco protocol. || Nous présentons AVISS, un outil pour l'analyse de protocoles de sécurité qui supporte l'intégration de logiciels implantant différentes techniques de recherche, permettant de les comparer systématiquement et quantitativement, et de tracer un chemin vers l

a – UNIVERSITY OF GENOVA
b – FREIBURG
c – INRIA
d – UNIVERSITE HENRI POINCARE
e – UNIVERSITE NANCY 2
1 : 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)

inria-00100915, version 1
http://hal.inria.fr/inria-00100915
oai:hal.inria.fr:inria-00100915
Contributeur : Publications Loria <>
Soumis le : Mardi 26 Septembre 2006, 14:52:52
Dernière modification le : Mercredi 17 Janvier 2007, 15:38:56

Voir la fiche détaillée

Exporter

Bibtex EndNote TEI RefWorks

%% inria-00100915, version 1
%% http://hal.inria.fr/inria-00100915
@inproceedings{armando:inria-00100915,
    hal_id = {inria-00100915},
    url = {http://hal.inria.fr/inria-00100915},
    title = {{The AVISS Security Protocol Analysis Tool}},
    author = {Armando, Alessandro and Basin, David and Bouallagui, Mehdi and Chevalier, Yannick and Compagna, Luca and Moedersheim, Sebastian and Rusinowitch, Micha{\"e}l and Turuani, Mathieu and Vigano, Luca and Vigneron, Laurent},
    abstract = {{We introduce AVISS, a tool for security protocol analysis that supports the integration of back-ends implementing different search techniques, allowing for their systematic and quandtitative comparison and paving the way to their effective interaction. As a significant example, we have implemented three back-ends, and used the AVISS tool to analyse and find flaws in 36 protocols, including 31 problems in the Clark-Jacob's protocol library and a previously unreported flaw in the Denning-Sacco protocol. || Nous pr{\'e}sentons AVISS, un outil pour l'analyse de protocoles de s{\'e}curit{\'e} qui supporte l'int{\'e}gration de logiciels implantant diff{\'e}rentes techniques de recherche, permettant de les comparer syst{\'e}matiquement et quantitativement, et de tracer un chemin vers l}},
    keywords = {cryptographic protocols; verification; model checking; theorem proving; sat solving || protocoles cryptographiques; v{\'e}rification; v{\'e}rification de mod{\`e}les; d{\'e}monstration automatique; probl{\`e}mes sat},
    language = {Anglais},
    affiliation = {CASSIS - INRIA Lorraine - LORIA / LIFC},
    booktitle = {{14th International Conference on Computer Aided Verification - CAV'2002}},
    publisher = {Springer},
    pages = {349-353},
    address = {Copenhaguen, Denmark},
    volume = {2404},
    editor = {Ed Brinksma and Kim Guldstrand Larsen },
    series = {Lecture Notes in Computer Science },
    note = {Colloque avec actes et comit{\'e} de lecture. internationale. A02-R-348 || armando02a A02-R-348 || armando02a },
    audience = {internationale },
    year = {2002},
    month = Jul,
}

<?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-00100915"><analytic>
<author><persName><forename>Alessandro</forename><surname>Armando</surname></persName></author>
<author><persName><forename>David</forename><surname>Basin</surname></persName></author>
<author><persName><forename>Mehdi</forename><surname>Bouallagui</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></author>
<author><persName><forename>Sebastian</forename><surname>Moedersheim</surname></persName></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>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>Luca</forename><surname>Vigano</surname></persName></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 AVISS Security Protocol Analysis Tool</title></analytic><monogr><meeting>14th International Conference on Computer Aided Verification - CAV'2002</meeting><imprint><publisher>Springer</publisher><pubPlace><settlement>Copenhaguen</settlement><country> Denmark</country></pubPlace><biblScope type="publicationDate">2002-07-00</biblScope><biblScope type="vol">2404</biblScope><biblScope type="pp">349-353</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00100915</idno></biblStruct>
</listBibl>
</listBibl>