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
-
CC BY
BibTeX
@misc{cryptoeprint:2005/171,
author = {Prateek Gupta and Vitaly Shmatikov},
title = {Towards computationally sound symbolic analysis of key exchange protocols},
howpublished = {Cryptology {ePrint} Archive, Paper 2005/171},
year = {2005},
url = {https://eprint.iacr.org/2005/171}
}
