Composition of Password-based Protocols

Céline Chevalier 1 Stéphanie Delaune 1 Steve Kremer 2 Mark D. Ryan 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 : Formal and symbolic techniques are extremely useful for modelling and analysing security protocols. They have helped to improve our understanding of such protocols, allowed us to discover aws, and they 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.\par 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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/hal-00878640
Contributor : Steve Kremer <>
Submitted on : Wednesday, October 7, 2015 - 4:11:13 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Friday, January 8, 2016 - 10:45:02 AM

File

CDKR-fmsd13.pdf
Files produced by the author(s)

Identifiers

Citation

Céline Chevalier, Stéphanie Delaune, Steve Kremer, Mark D. Ryan. Composition of Password-based Protocols. Formal Methods in System Design, Springer Verlag, 2013, 43 (3), pp.369-413. ⟨10.1007/s10703-013-0184-6⟩. ⟨hal-00878640⟩

Share

Metrics

Record views

540

Files downloads

872