Towards a Constrained-based Verification of Parameterized Cryptographic Protocols

Najah Chridi 1 Mathieu Turuani 1 Michael Rusinowitch 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 : Although many works have been dedicated to standard protocols like Needham-Schroeder very few address the more challenging class of group protocol s. 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. Our inference system generalizes the ones that are implemented in several tools for a bounded number of sessions and fixed size lists in message. In particular when applied to protocols whose specification does not contain unbounded lists our inference system provides a decision procedure for secrecy in the case of a fixed number of sessions.
Type de document :
Communication dans un congrès
Michael Hanus. 18th International Symposium on Logic-Based Program Synthesis and Transformation - LOPSTR 2008, Jul 2008, Valence, Spain. pp.191-206, 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00332484
Contributeur : Mathieu Turuani <>
Soumis le : vendredi 24 octobre 2008 - 16:29:39
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : lundi 7 juin 2010 - 21:00:31

Fichier

LOPSTR08-PostConference_Chridi...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00332484, version 1

Citation

Najah Chridi, Mathieu Turuani, Michael Rusinowitch. Towards a Constrained-based Verification of Parameterized Cryptographic Protocols. Michael Hanus. 18th International Symposium on Logic-Based Program Synthesis and Transformation - LOPSTR 2008, Jul 2008, Valence, Spain. pp.191-206, 2008. 〈inria-00332484〉

Partager

Métriques

Consultations de la notice

233

Téléchargements de fichiers

97