Safely composing security protocols

Véronique Cortier 1 Stéphanie Delaune 2
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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Security protocols are small programs that are executed in hostile environments. Many results and tools have been developed to formally analyze the security of a protocol in the presence of an active attacker that may block, intercept and send new messages. However even when a protocol has been proved secure, there is absolutely no guarantee if the protocol is executed in an environment where other protocols are executed, possibly sharing some common keys like public keys or long-term symmetric keys. In this paper, we show that security of protocols can be easily composed. More precisely, we show that whenever a protocol is secure, it remains secure even in an environment where arbitrary protocols satisfying a reasonable (syntactic) condition are executed. This result holds for a large class of security properties that encompasses secrecy and various formulations of authentication.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2009, 34 (1), pp.1--36. 〈10.1007/s10703-008-0059-4〉
Liste complète des métadonnées
Contributeur : Véronique Cortier <>
Soumis le : lundi 20 octobre 2008 - 16:34:53
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral



Véronique Cortier, Stéphanie Delaune. Safely composing security protocols. Formal Methods in System Design, Springer Verlag, 2009, 34 (1), pp.1--36. 〈10.1007/s10703-008-0059-4〉. 〈inria-00332354〉



Consultations de la notice