Céline Chevalier, Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Composition of Password-based Protocols. Formal Methods in System Design, 43(3):369–413, Springer, December 2013.
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 flaws, 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.
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.
@article{CDKR-fmsd13,
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 flaws, 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.},
author = {Chevalier, C{\'e}line and Delaune, St{\'e}phanie and
Kremer, Steve and Ryan, Mark D.},
OPTDOI = {10.1007/s10703-013-0184-6},
journal = {Formal Methods in System Design},
month = dec,
number = {3},
pages = {369-413},
publisher = {Springer},
title = {Composition of Password-based Protocols},
volume = {43},
year = {2013},
nmonth = {12},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}