Formal Modeling of Diffie-Hellman Derivability for Exploratory Automated Analysis

August 2013
Topics: Modeling and Simulation, Probability and Statistics, Theory of Computation
Moses D. Liskov, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
Download PDF (337.49 KB)

​In their groundbreaking paper, Diffie and Hellman proposed the first public-key operation, now known as the Diffie-Hellman key agreement protocol. Over three decades later, this protocol remains crucially important, a component of a great many cryptographic protocols. In this paper, we compare several models that capture the Diffie-Hellman protocol, with the aim of identifying a model that is both well-suited for automated protocol analysis and that has a strong, well-justified link to the model typically adopted in the computational complexity community.

We make two changes to this model: we replace computability with a Dolev-Yao style adversary, and we use non-standard analysis techniques to reduce the parametrized asymptotic setting to a simpler, singular one. The use of non-standard analysis helps justify our use of a hyperfinite field of exponents.​

Publications

Interested in MITRE's Work?

MITRE provides affordable, effective solutions that help the government meet its most complex challenges.
Explore Job Openings

Publication Search