Steve Kremer: Transforming Password Protocols to Compose

Transforming Password Protocols to Compose

Céline Chevalier, Stéphanie Delaune, and Steve Kremer. Transforming Password Protocols to Compose. In Proceedings of the 31st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), pp. 204–216, Leibniz International Proceedings in Informatics, Leibniz-Zentrum für Informatik, Mumbai, India, December 2011.

Download

[PDF] [PDF (long version)]

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.

BibTeX

@inproceedings{CDK-fsttcs11,
  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.\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.},
  address =       {Mumbai, India},
  author =        {Chevalier, C{\'e}line and Delaune, St{\'e}phanie and
                   Kremer, Steve},
  booktitle =     {{P}roceedings of the 31st {C}onference on
                   {F}oundations of {S}oftware {T}echnology and
                   {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  editor =        {Chakraborty, Supratik and Kumar, Amit},
  month =         dec,
  publisher =     {Leibniz-Zentrum f{\"u}r Informatik},
  series =        {Leibniz International Proceedings in Informatics},
  title =         {Transforming Password Protocols to Compose},
  year =          {2011},
  acronym =       {{FSTTCS}'11},
  nmonth =        {12},
  pages =         {204-216},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-fsttcs11.pdf},
}