Steve Kremer: From One Session to Many: Dynamic Tags for Security Protocols

From One Session to Many: Dynamic Tags for Security Protocols

Myrto Arapinis, Stéphanie Delaune, and Steve Kremer. From One Session to Many: Dynamic Tags for Security Protocols. In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), pp. 128–142, Lecture Notes in Artificial Intelligence 5330, Springer, Doha, Qatar, November 2008.
doi:10.1007/978-3-540-89439-1_9

Download

[PDF] [PDF (long version)] [HTML]

Abstract

The design and verification of cryptographic protocols is a notoriously difficult task, even in abstract Dolev-Yao models. This is mainly due to several sources of unboundedness (size of messages, number of sessions, ...). In this paper, we present a transformation which maps a protocol that is secure for a single session to a protocol that is secure for an unbounded number of sessions. The transformation is surprisingly simple, computationally light and works for arbitrary protocols that rely on usual cryptographic primitives, such as symmetric and asymmetric encryption as well as digital signatures. Our result provides an effective strategy to design secure protocols: (i) design a protocol intended to be secure for one session (this can be verified with existing automated tools); (ii) apply our transformation and obtain a protocol which is secure for an unbounded number of sessions. A side-effect of this result is that we characterize a class of protocols for which secrecy for an unbounded number of sessions is decidable.

BibTeX

@inproceedings{ADK-lpar08,
  abstract =      {The design and verification of cryptographic
                   protocols is a notoriously difficult task, even in
                   abstract Dolev-Yao models. This is mainly due to
                   several sources of unboundedness (size of messages,
                   number of sessions,~...). In~this paper, we~present a
                   transformation which maps a protocol that is secure
                   for a single session to a protocol that is secure for
                   an unbounded number of sessions. The~transformation
                   is surprisingly simple, computationally light and
                   works for arbitrary protocols that rely on usual
                   cryptographic primitives, such as symmetric and
                   asymmetric encryption as well as digital signatures.
                   Our~result provides an effective strategy to design
                   secure protocols: (i)~design a protocol intended to
                   be secure for one session (this can be verified with
                   existing automated tools); (ii)~apply our
                   transformation and obtain a protocol which is secure
                   for an unbounded number of sessions. A~side-effect of
                   this result is that we characterize a class of
                   protocols for which secrecy for an unbounded number
                   of sessions is decidable.},
  address =       {Doha, Qatar},
  author =        {Arapinis, Myrto and Delaune, St{\'e}phanie and
                   Kremer, Steve},
  booktitle =     {{P}roceedings of the 15th {I}nternational
                   {C}onference on {L}ogic for {P}rogramming,
                   {A}rtificial {I}ntelligence, and {R}easoning
                   ({LPAR}'08)},
  DOI =           {10.1007/978-3-540-89439-1_9},
  editor =        {Cervesato, Iliano and Veith, Helmut and
                   Voronkov, Andrei},
  month =         nov,
  pages =         {128-142},
  publisher =     {Springer},
  series =        {Lecture Notes in Artificial Intelligence},
  title =         {From One Session to Many: Dynamic Tags for Security
                   Protocols},
  volume =        {5330},
  year =          {2008},
  acronym =       {{LPAR}'08},
  nmonth =        {11},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ADK-lpar08.pdf},
}