Computational Diffie-Hellman (CDH) Assumption

The CDH assumption: given (g^a, g^b), compute the shared secret g^{ab}. This is the computational analogue of DDH; DDH ⟹ CDH but not vice versa.

Main definitions

• CDH_Game — the CDH game
• CDH_Advantage — probability of computing the shared secret
• CDHSecure — CDH hardness assumption
• DL_Adversary_DDH — discrete log adversary over DDHDef
• DL_Game_DDH — discrete log game over DDHDef
• cdh_of_dl_ddh — CDH adversary from DL adversary (CDH ⟹ DL reduction)

Cross-Validation

Property	This file	Textbook
Challenge	(g^a, g^b)	Boneh-Shoup Def. 11.1
Target	Compute ecdh(a, g^b) = g^{ab}	Compute g^{ab}
Group	DDHDef W	Cyclic group of prime order
CDH ⟹ DL	cdh_of_dl_ddh	BS Prop. 11.4

Equivalent formalizations:

• EasyCrypt: CDH theory in theories/crypto/DiffieHellman.ec
• SSProve (Rocq): not formalized (only DDH)

Relationship to other assumptions:

• DDH ⟹ CDH (if you can't distinguish, you can't compute)
• CDH ⟹ DL (if you can compute DH, you can compute discrete logs)
• co-CDH (in CoCDH.lean) is the Type-III bilinear variant

See also CDH_DL.lean for the CDH ⟹ DL reduction over PairingGroup.

References

• Boneh & Shoup, A Graduate Course in Applied Cryptography, §11.3, Def. 11.1; §11.3 Prop. 11.4
• Diffie & Hellman, New Directions in Cryptography, IEEE-IT 1976

CDH Game

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.CDH_Adversary (W : Type) : Type

CDH adversary: given (g^a, g^b), attempts to compute the shared secret ecdh(a, g^b) = g^{ab}.

Equations

• CatCrypt.Crypto.Assumptions.CDH_Adversary W = (W → W → CatCrypt.Core.SPComp W)

noncomputable def CatCrypt.Crypto.Assumptions.CDH_Game {W : Type} [SampleableType W] [DecidableEq W] (D : DDHDef W) (A : CDH_Adversary W) : Core.SPComp Bool

CDH game: sample key pairs (a, g^a) and (b, g^b), give (g^a, g^b) to adversary, check if output equals ecdh(a, g^b).

Returns true if the adversary computes the correct shared secret.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Crypto.Assumptions.CDH_Advantage {W : Type} [SampleableType W] [DecidableEq W] (D : DDHDef W) (A : CDH_Adversary W) : ENNReal

CDH advantage: probability that the adversary computes g^{ab}.

Equations

• CatCrypt.Crypto.Assumptions.CDH_Advantage D A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.CDH_Game D A) CatCrypt.Core.Heap.empty

def CatCrypt.Crypto.Assumptions.CDHSecure {W : Type} [SampleableType W] [DecidableEq W] (D : DDHDef W) (ε : ENNReal) : Prop

CDH hardness: all adversaries have bounded advantage.

Equations

• CatCrypt.Crypto.Assumptions.CDHSecure D ε = ∀ (A : CatCrypt.Crypto.Assumptions.CDH_Adversary W), CatCrypt.Crypto.Assumptions.CDH_Advantage D A ≤ ε

Reduction: DDH ⟹ CDH

If an adversary can compute g^{ab} (break CDH), it can also distinguish (g^a, g^b, g^{ab}) from (g^a, g^b, random) (break DDH), by computing the answer and comparing.

noncomputable def CatCrypt.Crypto.Assumptions.ddh_of_cdh {W : Type} [DecidableEq W] (A : CDH_Adversary W) : DDH_Adversary W

Construct a DDH adversary from a CDH adversary: compute the alleged shared secret and check if it matches the challenge.

Equations

• CatCrypt.Crypto.Assumptions.ddh_of_cdh A g_a g_b challenge = do let answer ← A g_a g_b CatCrypt.Core.SPComp.pure (decide (answer = challenge))

IsPure Proofs

theorem CatCrypt.Crypto.Assumptions.CDH_Game_isPure {W : Type} [SampleableType W] [DecidableEq W] (D : DDHDef W) (A : CDH_Adversary W) (hA : ∀ (x y : W), (A x y).IsPure) : (CDH_Game D A).IsPure

Reduction: CDH ⟹ DL (abstract DDHDef setting)

The standard direction: CDH hard implies DL hard (BS Prop. 11.4). Equivalently, by contrapositive: if you can solve DL (find private keys from public keys), you can solve CDH.

In the abstract DDHDef setting, a "discrete log adversary" receives a public key g^a and returns a private key a' such that the corresponding public key matches. We define this via keygen's structure: the adversary must recover the private component from the public component.

Reduction. Given a DL adversary that finds a from g^a:

1. Receive CDH challenge (g^a, g^b)
2. Run the DL adversary on g^a to recover a
3. Compute ecdh(a, g^b) = g^{ab}

This gives a CDH adversary whose advantage equals the DL advantage.

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.DL_Adversary_DDH (W : Type) : Type

DL adversary over abstract DDHDef: given a public key g^a, attempts to find the corresponding private key a.

Equations

• CatCrypt.Crypto.Assumptions.DL_Adversary_DDH W = (W → CatCrypt.Core.SPComp W)

noncomputable def CatCrypt.Crypto.Assumptions.DL_Game_DDH {W : Type} [SampleableType W] [DecidableEq W] (D : DDHDef W) (A : DL_Adversary_DDH W) : Core.SPComp Bool

DL game over abstract DDHDef: sample a key pair (a, g^a), give g^a to the adversary, check if the adversary's output a' yields the same public key (i.e., ecdh(a', G) = g^a conceptually, but since we only have ecdh : W → W → W, we check that the adversary can reproduce the DH shared secret).

Concretely: sample (a, g^a) and (b, g^b), give g^a to the adversary to get a', then check ecdh(a', g^b) = ecdh(a, g^b).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Crypto.Assumptions.DL_Advantage_DDH {W : Type} [SampleableType W] [DecidableEq W] (D : DDHDef W) (A : DL_Adversary_DDH W) : ENNReal

DL advantage over abstract DDHDef.

Equations

• CatCrypt.Crypto.Assumptions.DL_Advantage_DDH D A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.DL_Game_DDH D A) CatCrypt.Core.Heap.empty

noncomputable def CatCrypt.Crypto.Assumptions.cdh_of_dl_ddh {W : Type} [SampleableType W] (D : DDHDef W) (A_dl : DL_Adversary_DDH W) : CDH_Adversary W

Construct a CDH adversary from a DL adversary.

Given a DL adversary that finds private keys from public keys:

1. Receive (g^a, g^b)
2. Run the DL adversary on g^a to get candidate private key a'
3. Compute ecdh(a', g^b) as the alleged shared secret

Equations

• CatCrypt.Crypto.Assumptions.cdh_of_dl_ddh D A_dl g_a _g_b = do let a' ← A_dl g_a CatCrypt.Core.SPComp.pure (D.ecdh a' _g_b)

theorem CatCrypt.Crypto.Assumptions.dl_le_cdh_ddh {W : Type} [SampleableType W] [DecidableEq W] (D : DDHDef W) (A_dl : DL_Adversary_DDH W) : DL_Advantage_DDH D A_dl ≤ CDH_Advantage D (cdh_of_dl_ddh D A_dl)

CDH ⟹ DL bound: any DL adversary yields a CDH adversary with at least as much advantage.

CDH_Advantage D (cdh_of_dl_ddh D A_dl) ≥ DL_Advantage_DDH D A_dl

Equivalently (for the standard "hardness implies hardness" direction): DL_Advantage_DDH D A_dl ≤ CDH_Advantage D (cdh_of_dl_ddh D A_dl)

theorem CatCrypt.Crypto.Assumptions.cdh_secure_implies_dl_secure {W : Type} [SampleableType W] [DecidableEq W] (D : DDHDef W) (ε : ENNReal) (h_cdh : CDHSecure D ε) (A_dl : DL_Adversary_DDH W) : DL_Advantage_DDH D A_dl ≤ ε

Corollary: CDH security implies DL security.

If D is ε-CDH-secure, then for any DL adversary, the DL advantage is at most ε.