Skip to Main content Skip to Navigation
Conference papers

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Mathieu Turuani Connect in order to contact the contributor
Submitted on : Friday, October 24, 2008 - 4:29:39 PM
Last modification on : Saturday, October 16, 2021 - 11:26:06 AM
Long-term archiving on: : Monday, June 7, 2010 - 9:00:31 PM


Files produced by the author(s)


  • HAL Id : inria-00332484, version 1


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



Record views


Files downloads