Key Exchange Protocols: Security Definition, Proof Method and Applications

Anupam Datta; Ante Derek; John C.  Mitchell; Bogdan Warinschi

Paper 2006/056

Key Exchange Protocols: Security Definition, Proof Method and Applications

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

Abstract

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.

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Published elsewhere. Unknown where it was published
Contact author(s): aderek @ cs stanford edu
History: 2006-02-15: received
Short URL: https://ia.cr/2006/056
License: CC BY

BibTeX

@misc{cryptoeprint:2006/056,
      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},
      url = {https://eprint.iacr.org/2006/056}
}