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.
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.
@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)},
OPTDOI = {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},
OPTLONGPDF = {https://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
rr-lsv-2008-17.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}