From One Session to Many: Dynamic Tags for Security Protocols

Myrto Arapinis, Stéphanie Delaune, Steve Kremer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 characterize a class of protocols for which secrecy for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a 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 protocols: (i) design a protocol intended to be secure for one protocol 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. The proof of our result is closely tied to a particular constraint solving procedure by Comon-Lundh et al.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings
Place of PublicationBerlin, Heidelberg
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Electronic)978-3-540-89439-1
ISBN (Print)978-3-540-89438-4
Publication statusPublished - 2008

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'From One Session to Many: Dynamic Tags for Security Protocols'. Together they form a unique fingerprint.

Cite this