Welcome to the resource topic for 2005/171
Title:
Towards computationally sound symbolic analysis of key exchange protocols
Authors: Prateek Gupta, 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.
ePrint: https://eprint.iacr.org/2005/171
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .