Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder

Francis Klay 1 Judson Santiago 2 Laurent Vigneron 3
3 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, 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 its limits, we define a new method based on the handling of the knowledge of protocol participants. This method is very general and is of natural use, as it consists in adding simple annotations, like for authentication problems. The method 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 unknown 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 :
Rapport
[Research Report] RR-6324, INRIA. 2007, pp.22
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00179550
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 22 octobre 2007 - 08:39:29
Dernière modification le : jeudi 11 janvier 2018 - 06:20:00
Document(s) archivé(s) le : mardi 21 septembre 2010 - 14:40:11

Fichiers

RR-6324.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00179550, version 2
  • ARXIV : 0710.3305

Citation

Francis Klay, Judson Santiago, Laurent Vigneron. Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder. [Research Report] RR-6324, INRIA. 2007, pp.22. 〈inria-00179550v2〉

Partager

Métriques

Consultations de la notice

241

Téléchargements de fichiers

229