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.
Formal Modeling of Diffie-Hellman Derivability for Exploratory Automated Analysis
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.
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.