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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00426919
Contributor : Michaël Rusinowitch <>
Submitted on : Wednesday, October 28, 2009 - 3:04:06 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM

Identifiers

  • 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. pp.277-289. ⟨inria-00426919⟩

Share

Metrics

Record views

232