Steve Kremer: Dynamic Tags for Security Protocols

Dynamic Tags for Security Protocols

Myrto Arapinis, Stéphanie Delaune, and Steve Kremer. Dynamic Tags for Security Protocols. Logical Methods in Computer Science, 10(2), 2014.
doi:10.2168/LMCS-10(2:11)2014

Download

[PDF] [HTML]

Abstract

The design and verification of cryptographic protocols is a notoriously difficult task, even in symbolic models which take an abstract view of cryptography. This is mainly due to the fact that protocols may interact with an arbitrary attacker which yields a verification problem that has several sources of unboundedness (size of messages, number of sessions, etc. In this paper, we characterize a class of protocols for which deciding security for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a protocol that is secure for a bounded number of protocol sessions (a decidable problem) to a protocol that is secure for an unbounded number of sessions. The precise number of sessions that need to be considered is a function of the security property and we show that for several classical security properties a single session is sufficient. Therefore, in many cases our results yields a design strategy for security protocols: (i) design a protocol intended to be secure for a single session; and (ii) apply our transformation to obtain a protocol which is secure for an unbounded number of sessions.

BibTeX

@Article{ADK-lmcs14,
  abstract =     {The design and verification of cryptographic
                  protocols is a notoriously difficult task, even in
                  symbolic models which take an abstract view of
                  cryptography. This is mainly due to the fact that
                  protocols may interact with an arbitrary attacker
                  which yields a verification problem that has several
                  sources of unboundedness (size of messages, number
                  of sessions, etc.  In this paper, we characterize a
                  class of protocols for which deciding security for
                  an unbounded number of sessions is decidable. More
                  precisely, we present a simple transformation which
                  maps a protocol that is secure for a bounded number
                  of protocol sessions (a decidable problem) to a
                  protocol that is secure for an unbounded number of
                  sessions. The precise number of sessions that need
                  to be considered is a function of the security
                  property and we show that for several classical
                  security properties a single session is
                  sufficient. Therefore, in many cases our results
                  yields a design strategy for security protocols: (i)
                  design a protocol intended to be secure for a
                  {single session}; and (ii) apply our transformation
                  to obtain a protocol which is secure for an
                  unbounded number of sessions.},
  author = 	 {Arapinis, Myrto and Delaune, St{\'e}phanie
                  and Kremer, Steve},
  title = 	 {Dynamic Tags for Security Protocols},
  journal = 	 {Logical Methods in Computer Science},
  year = 	 {2014},
  DOI =          {10.2168/LMCS-10(2:11)2014},
  volume = 	 {10},
  number = 	 {2},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  url =           {http://lmcs-online.org/ojs/viewarticle.php?id=1284&layout=abstract},
}