The Diffie-Hellman Key-Agreement Scheme in the Strand-Space Model

By Jonathan Herzog

The Diffie-Hellman key exchange scheme is a standard component of cryptographic protocols.

Download Resources


PDF Accessibility

One or more of the PDF files on this page fall under E202.2 Legacy Exceptions and may not be completely accessible. You may request an accessible version of a PDF using the form on the Contact Us page.

The Diffie-Hellman key exchange scheme is a standard component of cryptographic protocols. In this paper, we propose a way in which protocols that use this computational primitive can be verified using formal methods. In particular, we separate the computational aspects of such an analysis from the formal aspects. First, we use Strand Space terminology to define a security condition that summarizes the security guarantees of Diffie-Hellman. Once this property is assumed, the analysis of a protocol is a purely formal enterprise. (We demonstrate the applicability and usefulness of this property by analyzing a sample protocol.) Furthermore, we show that this property is sound in the computational setting by mapping formal attacks to computational algorithms. We demonstrate that if there exists a formal attack that violates the formal security condition, then it maps to a computational algorithm that solves the Diffie-Hellman problem. Hence, if the Diffie-Hellman problem is hard, the security condition holds globally.