摘要 : 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 criteri... 展开 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. (c) 2004 Elsevier Inc. All rights reserved. 收起