  We extend symbolic protocol analysis to apply to protocols using
Diffie-Hellman operations. Diffie-Hellman operations act on a cyclic group of
prime order, together with an exponentiation operator. The exponents form a
finite field. This rich algebraic structure has resisted previous symbolic
approaches. We work in an algebra defined by the normal forms of a rewriting
theory (modulo associativity and commutativity). These normal forms allow us to
define our crucial notion of indicator, a vector of integers that summarizes
how many times each secret exponent appears in a message. We prove that the
adversary can never construct a message with a new indicator in our adversary
model. Using this invariant, we prove the main security goals achieved by
several different protocols that use Diffie-Hellman operators in subtle ways.
We also give a model-theoretic justification of our rewriting theory: the
theory proves all equations that are uniformly true as the order of the cyclic
group varies.
