Modeling Diffie-Hellman Derivability for Automated Analysis

Friday, May 23, 2014 - 10:30am to 12:00pm
32-G449 (Patil/Kiva)
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.