Sciweavers

CCS
2005
ACM

Towards computationally sound symbolic analysis of key exchange protocols

13 years 8 months ago
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.
Prateek Gupta, Vitaly Shmatikov
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CCS
Authors Prateek Gupta, Vitaly Shmatikov
Comments (0)