Skip to main content

Decidability for Implicitly Authenticated Diffie-Hellman Protocols

Joshua D. Guttman ( Worcester Polytechnic Institute and The MITRE Corporation )

Many protocols use the Diffie-Hellman method for key agreement, in combination with certified long-term values or digital signatures for authentication.  These protocols are intended to satisfy security goals such as key secrecy, forward secrecy, resistance to key compromise attacks and unknown key share attacks, and various flavors of authentication.  We express these security goals by formulas in a first-order language, which take a special form, namely as geometric sequents.

We prove it is decidable whether a protocol in a fairly inclusive class of DH protocols ("lightweight" protocols) achieves a given security goal.

Protocol executions form logical models (structures), and a counterexample to a security goal is a model in which the desired security goal is not satisfied.  Each model includes a cyclic group of a particular prime order q and a field of the same characteristic q, as is standard.

An adversary strategy succeeds if for infinitely many q, there are counter-models based on prime q, using this strategy. While apparently weaker than the full computational attacker, this adversary strengthens earlier work within algebraic or symbolic models.  Our decidability result depends on working directly within the natural algebraic structures (cyclic groups and fields), rather than within the equational theories that symbolic models have previously used.

 

 

Share this: