Decidability for Lightweight Diffie-Hellman Protocols

ABSTRACT. Many protocols use the Diffie-Hellman method for key agreement, in combination with certified long-term values or digital signatures for authentication. These protocols aim at security goals such as key secrecy, forward secrecy, resistance to key compromise attacks, and various flavors of authentication. However, analysis of these protocols has been challenging, both in the computational model and in the symbolic model. An obstacle in the symbolic model is the undecidability of unification in many theories such as rings.

In this paper, we develop an algebraic version of the symbolic approach, in which we work directly within finite fields. These are natural structures for the protocols. The adversary, in giving a counterexample to a protocol goal in a finite field, may rely on any identity in that field. He defeats the protocol if there are counterexamples in infinitely many finite fields.

We prove that, even for this strong adversary, security goals for a wide class of protocols are decidable.