Cryptology ePrint Archive: Report 2005/171

Towards computationally sound symbolic analysis of key exchange protocols

Prateek Gupta and Vitaly Shmatikov

Abstract: 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 sound abstractions of CMA-secure digital signatures and a restricted form of 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.

Category / Keywords: Cryptographic protocols / key exchange, formal methods, symbolic analysis

Publication Info: Extended abstract of this paper was published in the 3rd ACM Workshop on Formal Methods in Security Engineering

Date: received 9 Jun 2005, last revised 15 Sep 2005

Contact author: shmat at cs utexas edu

Available format(s): Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation

Version: 20050915:160056 (All versions of this report)

Short URL: ia.cr/2005/171

Discussion forum: Show discussion | Start new discussion