Abstraction and resolution modulo AC: How to verify Diffie-Hellman-like protocols automatically

We show how cryptographic protocols using Diffie-Hellman primitives, i.e., modular exponentiation on a fixed generator, can be encoded in Horn clauses modulo associativity and commutativity. In order to obtain a sufficient criterion of security, we design a complete (but not sound in general) resolution procedure for a class of flattened clauses modulo simple equational theories, including associativity-commutativity. We report on a practical implementation of this algorithm in the MOP modular platform for automated proving; in particular, we obtain the first fully automated proof of security of the IKA.1 initial key agreement protocol in the so-called pure eavesdropper model.