Decidable Analysis for a Class of Cryptographic Group Protocols with Unbounded Lists

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, very few address the more challenging class of group protocols. We investigated group protocol analysis in a synchronous model, that allows the specification of unbounded sets of agents with related behavior. Also, when used in an asychronous way, this generalizes standard protocol models with bounded number of agents by permitting unbounded lists inside messages (including unbounded number of variables, nonces, etc..). This approach also applies to analyzing Web services manipulating sequences of items. In this model we propose a decision procedure for the sub-class of well-tagged protocols with autonomous keys.
Type de document :
Communication dans un congrès
Computer Security Foundations Symposium, Jul 2009, Port Jefferson, United States. IEEE, pp.277-289, 2009, Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF'09)
Liste complète des métadonnées

https://hal.inria.fr/inria-00426919
Contributeur : Michaël Rusinowitch <>
Soumis le : mercredi 28 octobre 2009 - 15:04:06
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : inria-00426919, version 1

Citation

Najah Chridi, Mathieu Turuani, Michael Rusinowitch. Decidable Analysis for a Class of Cryptographic Group Protocols with Unbounded Lists. Computer Security Foundations Symposium, Jul 2009, Port Jefferson, United States. IEEE, pp.277-289, 2009, Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF'09). 〈inria-00426919〉

Partager

Métriques

Consultations de la notice

203