Cryptology ePrint Archive: Report 2019/526

Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman

Cas Cremers and Dennis Jackson

Abstract: Diffie-Hellman groups are a widely used component in cryptographic protocols in which a shared secret is needed. These protocols are typically proven to be secure under the assumption they are implemented with prime order Diffie Hellman groups. However, in practice, many implementations either choose to use non-prime order groups for reasons of efficiency, or can be manipulated into operating in non-prime order groups. This leaves a gap between the proofs of protocol security, which assume prime order groups, and the real world implementations. This is not merely a theoretical possibility: many attacks exploiting small subgroups or invalid curve points have been found in the real world.

While many advances have been made in automated protocol analysis, modern tools such as Tamarin and ProVerif represent DH groups using an abstraction of prime order groups. This means they, like many cryptographic proofs, may miss practical attacks on real world protocols.

In this work we develop a novel extension of the symbolic model of Diffie-Hellman groups. By more accurately modelling internal group structure, our approach captures many more differences between prime order groups and their actual implementations. The additional behaviours that our models capture are surprisingly diverse, and include not only attacks using small subgroups and invalid curve points, but also a range of proposed mitigation techniques, such as excluding low order elements, single coordinate ladders, and checking the elliptic curve equation. Our models thereby capture a large family of attacks that were previously outside the symbolic model.

We implement our improved models in the Tamarin prover. We find a new attack on the Secure Scuttlebutt Gossip protocol, independently discover a recent attack on Tendermintís secure handshake, and evaluate the effectiveness of the proposed mitigations for recent Bluetooth attacks.

Category / Keywords: cryptographic protocols / formal verification, symbolic model, tamarin prover, diffie-hellman groups

Original Publication (with minor differences): 32nd IEEE Computer Security Foundations Symposium, CSF 2019

Date: received 19 May 2019, last revised 19 May 2019

Contact author: dennis jackson at cs ox ac uk

Available format(s): PDF | BibTeX Citation

Version: 20190520:203513 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]