DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2011.204

Transforming Password Protocols to Compose

Authors: Céline Chevalier, Stéphanie Delaune, and Steve Kremer

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

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.

Cite as

Céline Chevalier, Stéphanie Delaune, and Steve Kremer. Transforming Password Protocols to Compose. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 204-216, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{chevalier_et_al:LIPIcs.FSTTCS.2011.204,
  author =	{Chevalier, C\'{e}line and Delaune, St\'{e}phanie and Kremer, Steve},
  title =	{{Transforming Password Protocols to Compose}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{204--216},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.204},
  URN =		{urn:nbn:de:0030-drops-33273},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.204},
  annote =	{Keywords: Security, cryptographic protocols, composition}
}

Search Results

Documents authored by Chevalier, Céline

Transforming Password Protocols to Compose

Abstract

Cite as

Thanks for your feedback!

Could not send message