Steve Kremer: Composition of Password-based Protocols

Composition of Password-based Protocols

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, 2013.
doi:10.1007/s10703-013-0184-6

Download

[PDF] [HTML]

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.
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.

BibTeX

@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 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.},
  author = 	 {Chevalier, C{\'e}line and Delaune, St{\'e}phanie
                  and Kremer, Steve and Ryan, Mark D.},
  title = 	 {Composition of Password-based Protocols},
  journal = 	 {Formal Methods in System Design},
  year = 	 {2013},
  DOI =          {10.1007/s10703-013-0184-6},
  volume = 	 {43},
  number = 	 {3},
  pages = 	 {369-413},
  url =           {https://members.loria.fr/skremer/files/Papers/CDKR-fmsd13.pdf},
}