International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Towards computationally sound symbolic analysis of key exchange protocols

Authors:
Prateek Gupta
Vitaly Shmatikov
Download:
URL: http://eprint.iacr.org/2005/171
Search ePrint
Search Google
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.
BibTeX
@misc{eprint-2005-12507,
  title={Towards computationally sound symbolic analysis of key exchange protocols},
  booktitle={IACR Eprint archive},
  keywords={Cryptographic protocols / key exchange, formal methods, symbolic analysis},
  url={http://eprint.iacr.org/2005/171},
  note={Extended abstract of this paper was published in the 3rd ACM Workshop on Formal Methods in Security Engineering shmat@cs.utexas.edu 13041 received 9 Jun 2005, last revised 15 Sep 2005},
  author={Prateek Gupta and Vitaly Shmatikov},
  year=2005
}