Modeling Diffie-Hellman Derivability for Automated Analysis

Friday, May 23, 2014 - 10:30am to 12:00pm

Location:

32-G449 (Patil/Kiva)

Speaker:

Moses Liskov, MITRE Corporation

Abstract: Automated analysis of protocols involving Diffie-

Hellman key exchange is challenging, in part because of the

undecidability of the unification problem in relevant theories. In

this paper, we justify the use of a more restricted theory that

includes multiplication of exponents but not addition, providing

unitary and efficient unification.

To justify this theory, we link it to a computational model

of non-uniform circuit complexity through several incremental

steps. First, we give a model closely analogous to the computational

model, in which derivability is modeled by closure under

simple algebraic transformations. This model retains many of the

complex features of the computational model, including defining

success based on asymptotic probability for a non-uniform family

of strategies. We describe an intermediate model based on formal

polynomial manipulations, in which success is exact and there

is no longer a parametrized notion of the strategy. Despite the

many differences in form, we are able to prove an equivalence

between the asymptotic and intermediate models by showing that

a sufficiently successful asymptotic strategy implies the existence

of a perfect strategy. Finally, we describe a symbolic model in

which addition of exponents is not modeled, and prove that (for

expressible problems), the symbolic model is equivalent to the

intermediate model.

Joint work with F. Javier Thayer.