Dynamic Tags for Security Protocols

Myrto Arapinis 1 Stéphanie Delaune 2 Steve Kremer 3
3 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : The design and verification of cryptographic protocols is a notoriously difficult task, even in symbolic models which take an abstract view of cryptography. This is mainly due to the fact that protocols may interact with an arbitrary attacker which yields a verification problem that has several sources of unboundedness (size of messages, number of sessions, etc. In this paper, we characterize a class of protocols for which deciding security for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a protocol that is secure for a bounded number of protocol sessions (a decidable problem) to a protocol that is secure for an unbounded number of sessions. The precise number of sessions that need to be considered is a function of the security property and we show that for several classical security properties a single session is sufficient. Therefore, in many cases our results yields a design strategy for security protocols: (i) design a protocol intended to be secure for a single session; and (ii) apply our transformation to obtain a protocol which is secure for an unbounded number of sessions.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 10 (2), pp.50. 〈10.2168/LMCS-10(2:11)2014〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01090766
Contributeur : Steve Kremer <>
Soumis le : jeudi 4 décembre 2014 - 10:46:33
Dernière modification le : jeudi 15 février 2018 - 08:48:14

Lien texte intégral

Identifiants

Citation

Myrto Arapinis, Stéphanie Delaune, Steve Kremer. Dynamic Tags for Security Protocols. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 10 (2), pp.50. 〈10.2168/LMCS-10(2:11)2014〉. 〈hal-01090766〉

Partager

Métriques

Consultations de la notice

248