Skip to Main content Skip to Navigation
Conference papers

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata
Contributor : Michaël Rusinowitch Connect in order to contact the contributor
Submitted on : Wednesday, October 28, 2009 - 3:04:06 PM
Last modification on : Friday, January 21, 2022 - 3:09:01 AM


  • HAL Id : inria-00426919, version 1


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⟩



Record views