Constraints-based Verification of Parameterized Cryptographic Protocols.

Najah Chridi 1, * Mathieu Turuani 1, * Michaël Rusinowitch 1, *
* Auteur correspondant
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 : Cryptographic protocols are crucial for securing electronic transactions. The confidence in these protocols can be increased by the formal analysis of their security properties. Although many works have been dedicated to standard protocols like Needham-Schroeder very few address the more challenging class of group protocols. We present a synchronous model for group protocols, that generalizes standard protocol models by permitting unbounded lists inside messages. In this extended model we propose a correct and complete set of inference rules for checking security properties in presence of an active intruder for the class of Well-Tagged protocols. We prove that the application of these rules on a constraint system terminates and that the normal form obtained can be checked for satisfiability. Therefore, we present here a decision procedure for this class.
Type de document :
Rapport
[Research Report] RR-6712, INRIA. 2008, pp.54
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00336539
Contributeur : Mathieu Turuani <>
Soumis le : mardi 4 novembre 2008 - 15:11:58
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : mardi 9 octobre 2012 - 15:00:25

Fichier

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

Identifiants

  • HAL Id : inria-00336539, version 1

Citation

Najah Chridi, Mathieu Turuani, Michaël Rusinowitch. Constraints-based Verification of Parameterized Cryptographic Protocols.. [Research Report] RR-6712, INRIA. 2008, pp.54. 〈inria-00336539〉

Partager

Métriques

Consultations de la notice

308

Téléchargements de fichiers

115