Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
The authors present a general approach for the symbolic analysis of security protocols that use Diffie-Hellman exponentiation to achieve advanced security properties. They model protocols as multi-set rewriting systems and security properties as first-order formulas. They analyze them using a novel constraint-solving algorithm that supports both falsification and verification, even in the presence of an unbounded number of protocol sessions. The algorithm exploits the finite variant property and builds on ideas from strand spaces and proof normal forms. They demonstrate the scope and the effectiveness of their algorithm on non-trivial case studies. For example, the algorithm successfully verifies the NAXOS protocol with respect to a symbolic version of the eCK security model.