Safely Composing Security Protocols

Safely Composing Security Protocols. Véronique Cortier, Jérémie Delaitre, and Stéphanie Delaune. In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), pp. 352–363, Lecture Notes in Computer Science 4855, Springer, New Delhi, India, December 2007.

Download

[PDF] [HTML]

Abstract

Security protocols are small programs that are executed in hostile environments. Many results and tools have been developed to formally analyze the security of a protocol in the presence of active attackers that may block, intercept and send new messages. However even when a protocol has been proved secure, there is absolutely no guarantee if the protocol is executed in an environment where other protocols, possibly sharing some common identities and keys like public keys or long-term symmetric keys, are executed.
In this paper, we show that security of protocols can be easily composed. More precisely, we show that whenever a protocol is secure, it remains secure even in an environment where arbitrary protocols are executed, provided each encryption contains some tag identifying each protocol, like e.g. the name of the protocol.

BibTeX

@inproceedings{CDD-fsttcs07,
  address =       {New~Delhi, India},
  author =        {Cortier, V{\'e}ronique and Delaitre, J{\'e}r{\'e}mie and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 27th {C}onference on
                   {F}oundations of {S}oftware {T}echnology and
                   {T}heoretical {C}omputer {S}cience ({FSTTCS}'07)},
  editor =        {Arvind, V. and Prasad, Sanjiva},
  month =         dec,
  pages =         {352-363},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Safely Composing Security Protocols},
  volume =        {4855},
  year =          {2007},
  abstract =      {Security protocols are small programs that are
                   executed in hostile environments. Many results and
                   tools have been developed to formally analyze the
                   security of a protocol in the presence of active
                   attackers that may block, intercept and send new
                   messages. However even when a protocol has been
                   proved secure, there is absolutely no guarantee if
                   the protocol is executed in an environment where
                   other protocols, possibly sharing some common
                   identities and keys like public keys or long-term
                   symmetric keys, are executed.\par In this paper, we
                   show that security of protocols can be easily
                   composed. More precisely, we show that whenever a
                   protocol is secure, it remains secure even in an
                   environment where arbitrary protocols are executed,
                   provided each encryption contains some tag
                   identifying each protocol, like e.g.~the name of the
                   protocol.},
  doi =           {10.1007/978-3-540-77050-3_29},
}