Automated Unbounded Verification of Security Protocols

Yannick Chevalier 1 Laurent Vigneron 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a new model for automated verification of security protocols, permitting the use of an unbounded number of protocol runs. We prove its correctness, completeness and also that it terminates. It has been implemented and its efficiency is clearly shown by the number of protocols successfully studied. In particular, we present an attack previously unreported on the Denning-Sacco symmetric key protocol. || Nous présentons un nouveau modèle pour la vérification automatique de protocoles de sécurité, permettant l'utilisation d'un nombre non borné d'exécutions du protocole. Nous démontrons sa correction, sa complétude et sa terminaison. Il a été implanté et s
Type de document :
Communication dans un congrès
Ed Brinksma and Kim Guldstrand Larsen. 14th International Conference on Computer Aided Verification - CAV'2002, 2002, Copenhaguen, Denmark, Springer, 2404, pp.324-337, 2002, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00100916
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:52:53
Dernière modification le : vendredi 6 juillet 2018 - 15:06:09

Identifiants

  • HAL Id : inria-00100916, version 1

Citation

Yannick Chevalier, Laurent Vigneron. Automated Unbounded Verification of Security Protocols. Ed Brinksma and Kim Guldstrand Larsen. 14th International Conference on Computer Aided Verification - CAV'2002, 2002, Copenhaguen, Denmark, Springer, 2404, pp.324-337, 2002, Lecture Notes in Computer Science. 〈inria-00100916〉

Partager

Métriques

Consultations de la notice

166