Protocol composition for arbitrary primitives

Protocol composition for arbitrary primitives. Ștefan Ciobâcă and Véronique Cortier. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10), pp. 322–336, IEEE Computer Society Press, Edinburgh, Scotland, UK, July 2010. Erratum.

Download

[PDF] [HTML]

Abstract

We study the composition of security protocols when protocols share secrets such as keys. We show (in a Dolev-Yao model) that if two protocols use disjoint cryptographic primitives, their composition is secure if the individual protocols are secure, even if they share data. Our result holds for any cryptographic primitives that can be modeled using equational theories, such as encryption, signature, MAC, exclusive-or, and Diffie-Hellman. Our main result transforms any attack trace of the combined protocol into an attack trace of one of the individual protocols. This allows various ways of combining protocols such as sequentially or in parallel, possibly with inner replications. As an application, we show that a protocol using preestablished keys may use any (secure) key-exchange protocol without jeopardizing its security, provided that they do not use the same primitives. This allows us, for example, to securely compose a Diffie-Hellman key exchange protocol with any other protocol using the exchanged key, provided that the second protocol does not use the Diffie-Hellman primitives. We also explore tagging, which is a way of forcing the disjointness of two protocols that share cryptographic primitives We explain why composing protocols which use tagged cryptographic primitives like encryption and hash functions is secure by reducing this problem to the previous one.

BibTeX

@inproceedings{CC-csf10,
  address =       {Edinburgh, Scotland, UK},
  author =        {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and
                   Cortier, V{\'e}ronique},
  booktitle =     {{P}roceedings of the 23rd {IEEE} {C}omputer
                   {S}ecurity {F}oundations {S}ymposium ({CSF}'10)},
  month =         jul,
  pages =         {322-336},
  publisher =     {{IEEE} Computer Society Press},
  title =         {Protocol composition for arbitrary primitives},
  year =          {2010},
  abstract =      {We study the composition of security protocols when
                   protocols share secrets such as keys. We show (in a
                   Dolev-Yao model) that if two protocols use disjoint
                   cryptographic primitives, their composition is secure
                   if the individual protocols are secure, even if they
                   share data. Our result holds for any cryptographic
                   primitives that can be modeled using equational
                   theories, such as encryption, signature, MAC,
                   exclusive-or, and Diffie-Hellman. Our main result
                   transforms any attack trace of the combined protocol
                   into an attack trace of one of the individual
                   protocols. This allows various ways of combining
                   protocols such as sequentially or in parallel,
                   possibly with inner replications. As an application,
                   we show that a protocol using preestablished keys may
                   use any (secure) key-exchange protocol without
                   jeopardizing its security, provided that they do not
                   use the same primitives. This allows us, for example,
                   to securely compose a Diffie-Hellman key exchange
                   protocol with any other protocol using the exchanged
                   key, provided that the second protocol does not use
                   the Diffie-Hellman primitives. We also explore
                   tagging, which is a way of forcing the disjointness
                   of two protocols that share cryptographic primitives
                   We explain why composing protocols which use tagged
                   cryptographic primitives like encryption and hash
                   functions is secure by reducing this problem to the
                   previous one.},
		   note = {<a href="https://members.loria.fr/VCortier/files/Papers/erratum.pdf">Erratum</a>},
  doi =           {10.1109/CSF.2010.29},
}