Diffie-Hellman groups are commonly used in cryptographic protocols. While most state-of-the-art, symbolic protocol verifiers support them to some degree, they do not support all mathematical operations possible in these groups. In particular, they lack support for exponent addition, as these tools reason about terms using unification, which is undecidable in the theory describing all Diffie-Hellman operators. In this paper we approximate such a theory and propose a semi-decision procedure to determine whether a protocol, which may use all operations in such groups, satisfies user-defined properties. We implement this approach by extending the Tamarin prover to support the full Diffie-Hellman theory, including group element multiplication and hence addition of exponents. This is the first time a state-of-the-art tool can model and reason about such protocols. We illustrate our approach's effectiveness with different case studies: ElGamal encryption and MQV. Using Tamarin, we prove security properties of ElGamal, and we rediscover known attacks on MQV.

翻译：Diffie-Hellman群在密码协议中被广泛使用。尽管大多数先进的符号协议验证工具在一定程度上支持这些群，但它们并未支持这些群中所有可能的数学运算。具体而言，这些工具缺乏对指数加法的支持，因为它们使用合一推理来对项进行推理，而在描述所有Diffie-Hellman算子的理论中，合一是不可判定的。在本文中，我们近似了这样一个理论，并提出了一种半判定程序，用于确定一个可能使用此类群中所有运算的协议是否满足用户定义的属性。我们通过扩展Tamarin证明器以支持完整的Diffie-Hellman理论（包括群元素乘法以及由此实现的指数加法）来实现这一方法。这是首次有先进工具能够建模并推理此类协议。我们通过不同的案例研究（ElGamal加密和MQV）展示了我们方法的有效性。利用Tamarin，我们证明了ElGamal的安全性属性，并重新发现了MQV的已知攻击。