Beyond the Finite Variant Property: Extending Symbolic Diffie-Hellman Group Models (Extended Version)

TL;DR

This paper extends symbolic protocol verification to fully support Diffie-Hellman groups, including exponent addition, enabling more accurate security analysis of protocols like ElGamal and MQV.

Contribution

It introduces a semi-decision procedure and extends the Tamarin prover to model all Diffie-Hellman operations, including exponent addition, which was previously unsupported.

Findings

Successfully modeled ElGamal encryption and proved its security.

Discovered known attacks on MQV using the extended model.

First tool to fully support Diffie-Hellman group operations in symbolic verification.

Abstract

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.