Towards computationally sound symbolic analysis of key exchange protocols

d abstract) Prateek Gupta and Vitaly Shmatikov The University of Texas at Austin We present a cryptographically sound formal method for proving correctness of key exchange protocols. Our main tool is a fragment of a symbolic protocol logic. We demonstrate that proofs of key agreement and key secrecy in this logic imply simulatability in Shoup’s secure multi-party framework for key exchange. As part of the logic, we present cryptographically stractions of CMA-secure digital signatures and Diffie-Hellman exponentiation, which is a technical result of independent interest. We illustrate our method by constructing a proof of security for a simple authenticated Diffie-Hellman protocol.

• Type: Conference
• Year: 2005
• Where: CCS
• Authors: Prateek Gupta, Vitaly Shmatikov
• Keywords: CCS 2005, Key Exchange, Key Exchange Protocols, Security Privacy, Symbolic Protocol Logic