From One Session to Many: Dynamic Tags for Security Protocols

Myrto Arapinis; Stéphanie Delaune; Steve Kremer

doi:10.1007/978-3-540-89439-1_9

From One Session to Many: Dynamic Tags for Security Protocols

Myrto Arapinis, Stéphanie Delaune, Steve Kremer

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 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 language	English
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication	15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings
Place of Publication	Berlin, Heidelberg
Publisher	Springer-Verlag GmbH
Pages	128-142
Number of pages	15
Volume	5330
ISBN (Electronic)	978-3-540-89439-1
ISBN (Print)	978-3-540-89438-4
DOIs	https://doi.org/10.1007/978-3-540-89439-1_9
Publication status	Published - 2008

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	5330
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-540-89439-1_9

http://dx.doi.org/10.1007/978-3-540-89439-1_9

Cite this

Arapinis, M., Delaune, S., & Kremer, S. (2008). From One Session to Many: Dynamic Tags for Security Protocols. In Logic for Programming, Artificial Intelligence, and Reasoning: 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings (Vol. 5330, pp. 128-142). (Lecture Notes in Computer Science; Vol. 5330). Springer-Verlag GmbH. https://doi.org/10.1007/978-3-540-89439-1_9

Arapinis, Myrto ; Delaune, Stéphanie ; Kremer, Steve. / From One Session to Many : Dynamic Tags for Security Protocols. Logic for Programming, Artificial Intelligence, and Reasoning: 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. Vol. 5330 Berlin, Heidelberg : Springer-Verlag GmbH, 2008. pp. 128-142 (Lecture Notes in Computer Science).

@inproceedings{61ac6189a23144139642e377cfab6079,

title = "From One Session to Many: Dynamic Tags for Security Protocols",

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 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.",

author = "Myrto Arapinis and St{\'e}phanie Delaune and Steve Kremer",

year = "2008",

doi = "10.1007/978-3-540-89439-1_9",

language = "English",

isbn = "978-3-540-89438-4",

volume = "5330",

series = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag GmbH",

pages = "128--142",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning",

}

Arapinis, M, Delaune, S & Kremer, S 2008, From One Session to Many: Dynamic Tags for Security Protocols. in Logic for Programming, Artificial Intelligence, and Reasoning: 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. vol. 5330, Lecture Notes in Computer Science, vol. 5330, Springer-Verlag GmbH, Berlin, Heidelberg, pp. 128-142. https://doi.org/10.1007/978-3-540-89439-1_9

From One Session to Many : Dynamic Tags for Security Protocols. / Arapinis, Myrto; Delaune, Stéphanie; Kremer, Steve.

Logic for Programming, Artificial Intelligence, and Reasoning: 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. Vol. 5330 Berlin, Heidelberg : Springer-Verlag GmbH, 2008. p. 128-142 (Lecture Notes in Computer Science; Vol. 5330).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - From One Session to Many

T2 - Dynamic Tags for Security Protocols

AU - Arapinis, Myrto

AU - Delaune, Stéphanie

AU - Kremer, Steve

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-89439-1_9

DO - 10.1007/978-3-540-89439-1_9

M3 - Conference contribution

SN - 978-3-540-89438-4

VL - 5330

T3 - Lecture Notes in Computer Science

SP - 128

EP - 142

BT - Logic for Programming, Artificial Intelligence, and Reasoning

PB - Springer-Verlag GmbH

CY - Berlin, Heidelberg

ER -

Arapinis M, Delaune S, Kremer S. From One Session to Many: Dynamic Tags for Security Protocols. In Logic for Programming, Artificial Intelligence, and Reasoning: 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. Vol. 5330. Berlin, Heidelberg: Springer-Verlag GmbH. 2008. p. 128-142. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-89439-1_9

From One Session to Many: Dynamic Tags for Security Protocols

Abstract

Publication series

Access to Document

Fingerprint

Cite this