Paper 2006/056

Key Exchange Protocols: Security Definition, Proof Method and Applications

Anupam Datta, Ante Derek, John C. Mitchell, and Bogdan Warinschi


We develop a compositional method for proving cryptographically sound security properties of key exchange protocols, based on a symbolic logic that is interpreted over conventional runs of a protocol against a probabilistic polynomial-time attacker. Since key indistinguishability and other previous specifications of secure key exchange suffer from specific compositionality problems, we develop a suitable specification of acceptable key generation. This definition is based on a simple game played by an adversary against a key exchange protocol and a conventional challenger characterizing secure encryption (or other primitives of interest). The method is illustrated using a sample protocol.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. Unknown where it was published
Contact author(s)
aderek @ cs stanford edu
2006-02-15: received
Short URL
Creative Commons Attribution


      author = {Anupam Datta and Ante Derek and John C.  Mitchell and Bogdan Warinschi},
      title = {Key Exchange Protocols: Security Definition, Proof Method and Applications},
      howpublished = {Cryptology ePrint Archive, Paper 2006/056},
      year = {2006},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.