Paper 2010/303

Universally Composable Symbolic Analysis of Diffie-Hellman based Key Exchange

Ran Canetti and Sebastian Gajek


Canetti and Herzog (TCC'06) show how to efficiently perform fully automated, computationally sound security analysis of key exchange protocols with an unbounded number of sessions. A key tool in their analysis is {\em composability}, which allows deducing security of the multi-session case from the security of a single session. However, their framework only captures protocols that use public key encryption as the only cryptographic primitive, and only handles static corruptions. We extend the [CH'06] modeling in two ways. First, we handle also protocols that use digital signatures and Diffie-Hellman exchange. Second, we handle also forward secrecy under fully adaptive party corruptions. This allows us to automatically analyze systems that use an unbounded number of sessions of realistic key exchange protocols such as the ISO 9798-3 or TLS protocol. A central tool in our treatment is a new abstract modeling of plain Diffie-Hellman key exchange. Specifically, we show that plain Diffie-Hellman securely realizes an idealized version of Key Encapsulation.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. Unknown where it was published
Automated ProofsUniversal CompositionDiffie-Hellman key exchangeforward secrecy
Contact author(s)
gajek @ post tau ac il
2010-05-25: received
Short URL
Creative Commons Attribution


      author = {Ran Canetti and Sebastian Gajek},
      title = {Universally Composable Symbolic Analysis of Diffie-Hellman based Key Exchange},
      howpublished = {Cryptology ePrint Archive, Paper 2010/303},
      year = {2010},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.