The Diffie-Hellman Key-Agreement Scheme in the Strand-Space Model
September 2003
Jonathan C. Herzog, The MITRE Corporation
ABSTRACT
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.
Additional Search Keywords
n/a
|
