Transforming Password Protocols to Compose

Céline Chevalier 1 Stéphanie Delaune 1, 2 Steve Kremer 2, 3
2 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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 (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Formal, symbolic techniques are extremely useful for modelling and analysing security protocols. They improved our understanding of security protocols, allowed to discover flaws, and also provide support for protocol design. However, such analyses usually consider that the protocol is executed in isolation or assume a bounded number of protocol sessions. Hence, no security guarantee is provided when the protocol is executed in a more complex environment. In this paper, we study whether password protocols can be safely composed, even when a same password is reused. More precisely, we present a transformation which maps a password protocol that is secure for a single protocol session (a decidable problem) to a protocol that is secure for an unbounded number of sessions. Our result provides an effective strategy to design secure password protocols: (i) design a protocol intended to be secure for one protocol session; (ii) apply our transformation and obtain a protocol which is secure for an unbounded number of sessions. Our technique also applies to compose different password protocols allowing us to obtain both inter-protocol and inter-session composition.
Type de document :
Communication dans un congrès
31st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), Dec 2011, Mumbai, India. 2011
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00636753
Contributeur : Steve Kremer <>
Soumis le : mercredi 7 octobre 2015 - 15:56:53
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : vendredi 8 janvier 2016 - 10:43:57

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00636753, version 1

Citation

Céline Chevalier, Stéphanie Delaune, Steve Kremer. Transforming Password Protocols to Compose. 31st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), Dec 2011, Mumbai, India. 2011. 〈inria-00636753〉

Partager

Métriques

Consultations de la notice

194

Téléchargements de fichiers

53