You are looking at a specific version 20050915:160056 of this paper. See the latest version.

Paper 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.

Metadata
Available format(s)
PDF PS
Category
Cryptographic protocols
Publication info
Published elsewhere. Extended abstract of this paper was published in the 3rd ACM Workshop on Formal Methods in Security Engineering
Keywords
key exchangeformal methodssymbolic analysis
Contact author(s)
shmat @ cs utexas edu
History
2005-09-15: last of 9 revisions
2005-06-10: received
See all versions
Short URL
https://ia.cr/2005/171
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.