Enrich-by-need Protocol Analysis for Diffie-Hellman (Extended Version)

TL;DR

This paper extends the enrich-by-need protocol analysis method to Diffie-Hellman key exchange, providing a reliable, algebraically justified, and efficient analysis framework within CPSA for protocols using DH.

Contribution

It introduces an algebraically natural model for analyzing Diffie-Hellman within enrich-by-need analysis, enhancing reliability and efficiency of CPSA.

Findings

Successfully analyzed Diffie-Hellman protocols using the new model

Provided an efficient unification method for the algebraic structure

Demonstrated the framework's reliability and informativeness

Abstract

Enrich-by-need protocol analysis is a style of symbolic protocol analysis that characterizes all executions of a protocol that extend a given scenario. In effect, it computes a strongest security goal the protocol achieves in that scenario. CPSA, a Cryptographic Protocol Shapes Analyzer, implements enrich-by-need protocol analysis. In this paper, we describe how to analyze protocols using the Diffie-Hellman mechanism for key agreement (DH) in the enrich-by-need style. DH, while widespread, has been challenging for protocol analysis because of its algebraic structure. DH essentially involves fields and cyclic groups, which do not fit the standard foundational framework of symbolic protocol analysis. By contrast, we justify our analysis via an algebraically natural model. This foundation makes the extended CPSA implementation reliable. Moreover, it provides informative and efficient results. An appendix explains how unification is efficiently done in our framework.