Skip to Main content Skip to Navigation
Journal articles

Deciding security properties for cryptographic protocols. Application to key cycles.

Hubert Comon-Lundh 1 Véronique Cortier 2 Eugen Zalinescu 3
2 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 : There is a large amount of work dedicated to the formal verification of security protocols. In this paper, we revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraint formalism for modeling security protocols. Our first contribution is to give a simple set of constraint simplification rules, that allows to reduce any deducibility constraint to a set of solved forms, representing all solutions (within the bound on sessions). As a consequence, we prove that deciding the existence of key cycles is NP-complete for a bounded number of sessions. The problem of key-cycles has been put forward by recent works relating computational and symbolic models. The so-called soundness of the symbolic model requires indeed that no key cycle (e.g., enc(k; k)) ever occurs in the execution of the protocol. Otherwise, stronger security assumptions (such as KDM-security) are required. We show that our decision procedure can also be applied to prove again the decidability of authentication-like properties and the decidability of a significant fragment of protocols with timestamps.
Document type :
Journal articles
Complete list of metadata
Contributor : Véronique Cortier Connect in order to contact the contributor
Submitted on : Tuesday, October 12, 2010 - 4:43:56 PM
Last modification on : Thursday, January 13, 2022 - 12:00:10 PM



Hubert Comon-Lundh, Véronique Cortier, Eugen Zalinescu. Deciding security properties for cryptographic protocols. Application to key cycles.. ACM Transactions on Computational Logic, Association for Computing Machinery, 2010, 11 (2), pp.Article 9. ⟨10.1145/1656242.1656244⟩. ⟨inria-00525775⟩



Les métriques sont temporairement indisponibles