Decidability for lightweight Diffie-Hellman protocols

DJ Dougherty, JD Guttman - 2014 IEEE 27th Computer Security …, 2014 - ieeexplore.ieee.org
2014 IEEE 27th Computer Security Foundations Symposium, 2014ieeexplore.ieee.org
Many protocols use Diffie-Hellman key agreement, combined 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, these protocols are challenging to analyze, both in computational
and symbolic models. An obstacle in the symbolic model is the undecidability of unification
in many theories in the signature of rings. In this paper, we develop an algebraic version of …
Many protocols use Diffie-Hellman key agreement, combined 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, these protocols are challenging to analyze, both in computational and symbolic models. An obstacle in the symbolic model is the undecidability of unification in many theories in the signature of rings. In this paper, we develop an algebraic version of the symbolic approach, working directly within finite fields, the natural structures for the protocols. The adversary, in giving an attack on a protocol goal in a finite field, may rely on any identity in that field. He defeats the protocol if there are attacks in infinitely many finite fields. We prove that, even for this strong adversary, security goals for a wide class of protocols are decidable.
ieeexplore.ieee.org