Automatic Methods for Analyzing Non-repudiation Protocole with an Active Intruder

Francis Klay 1 Laurent Vigneron 2
2 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 : Non-repudiation protocols have an important role in many areas where secured transactions with proofs of participation are necessary. Formal methods are clever and without error, therefore using them for verifying such protocols is crucial. In this purpose, we show how to partially represent non-repudiation as a combination of authentications on the Fair Zhou-Gollmann protocol. After discussing the limitations of this method, we define a new one based on the handling of the knowledge of protocol participants. This second method is general and of natural use, as it consists in adding simple annotations in the protocol specification. It is very easy to implement in tools able to handle participants knowledge. We have implemented it in the AVISPA Tool and analyzed the optimistic Cederquist-Corin-Dashti protocol, discovering two attacks. This extension of the AVISPA Tool for handling non-repudiation opens a highway to the specification of many other properties, without any more change in the tool itself.
Type de document :
Communication dans un congrès
Pierpaolo Degano, Joshua D. Guttman and Fabio Martinelli. 5th International Workshop on Formal Aspects in Security and Trust - FAST 2008, Oct 2008, Malaga, Spain. Springer-Verlag, 5491, pp.192-209, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-01465-9_13〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00376450
Contributeur : Laurent Vigneron <>
Soumis le : vendredi 17 avril 2009 - 15:18:44
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : vendredi 12 octobre 2012 - 16:51:02

Fichier

paperKV-LNCS5491.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Francis Klay, Laurent Vigneron. Automatic Methods for Analyzing Non-repudiation Protocole with an Active Intruder. Pierpaolo Degano, Joshua D. Guttman and Fabio Martinelli. 5th International Workshop on Formal Aspects in Security and Trust - FAST 2008, Oct 2008, Malaga, Spain. Springer-Verlag, 5491, pp.192-209, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-01465-9_13〉. 〈inria-00376450〉

Partager

Métriques

Consultations de la notice

539

Téléchargements de fichiers

162