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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2010, 11 (2), pp.Article 9. 〈10.1145/1656242.1656244〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00525775
Contributeur : Véronique Cortier <>
Soumis le : mardi 12 octobre 2010 - 16:43:56
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral

Identifiants

Citation

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〉

Partager

Métriques

Consultations de la notice

324