Formal Modeling of Diffie-Hellman Derivability for Exploratory Automated Analysis.

摘要

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. The core goal of any such model is to express the concept of derivability: values that can be produced by the model attacker. We start with the computational complexity view of a non- uniform adversary, in which derivability is defined by what can be computed with non- negligible probability by a polynomially bounded non-uniform family of circuits. In this paper we justify a simple algebra for the modeling of Di e- Hellman protocols. The algebra represents multiplication of exponents and exponentiation but does not represent addition of exponents or multiplication of bases. We justify our model by linking it to a standard computational model, and show a link between the concept of derivability in the computational model and in our model. The link involves two transformations of the model: a Dolev- Yao-style formalization and a generalization to hyper nite parameters. We show that either order of these two steps leads to the same notion of derivability. We then consider the restriction to monomial derivations (that is, derivations that act as monomials on exponents) and show a conservative extension result, 19 namely, that the fuller model including multiplication of bases and addition of exponents is a conservative extension of our restricted model. This allows us to conclude that for problems that may be expressed in our restricted model, derivability.