Selected publications at LSV: 2008

M. Arapinis, S. Delaune and S. KremerFrom One Session to Many: Dynamic Tags for Security ProtocolsIn Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), Doha, Qatar, November 2008, LNAI 5330, pages 128-142. Springer. ( PDF | PDF (long version) )
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},
   url = {},
   volume = {5330},
   year = {2008},

About LSV