Discrete Logarithm Assumptions (DLog / CDH / DDH)

Standard hardness assumptions for cryptographic groups, formalized using Mathlib's Module F G for scalar multiplication.

Mathematical setup

We model a cyclic group as:

• F : the scalar field (exponents), e.g. ZMod p for a prime-order group
• G : the group of elements (e.g. elliptic curve points), with [AddCommGroup G]
• Module F G : scalar multiplication a • g (corresponds to g^a in multiplicative notation)
• g : G : a fixed generator (public system parameter)

Notation correspondence

Textbook (multiplicative)	This file (additive / EC-style)
g^a	a • g
g^a · g^b = g^{a+b}	a • g + b • g = (a + b) • g
(g^a)^b = g^{ab}	b • (a • g) = (b * a) • g

Assumptions

• DLog: given (g, x • g), find x
• CDH: given (g, a • g, b • g), find (a * b) • g
• DDH: distinguish (g, a • g, b • g, (a * b) • g) from (g, a • g, b • g, c • g)

DLog (Discrete Logarithm)

def DiffieHellman.DLogAdversary (F G : Type) : Type

A DLog adversary receives a generator and a group element, and tries to find the discrete logarithm (scalar).

def DiffieHellman.dlogExp {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [DecidableEq F] [SampleableType F] (g : G) (adversary : DLogAdversary F G) : ProbComp Bool

DLog experiment: sample a random scalar x, give the adversary (g, x • g), and check whether the adversary's guess equals x.

CDH (Computational Diffie-Hellman)

def DiffieHellman.CDHAdversary (_F G : Type) : Type

A CDH adversary receives (g, a • g, b • g) and tries to compute (a * b) • g. _F is a phantom type parameter for the scalar field, enabling Lean to infer F at call sites of cdhExp.

def DiffieHellman.cdhExp {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] [DecidableEq G] (g : G) (adversary : CDHAdversary F G) : ProbComp Bool

CDH experiment: sample random scalars a, b, give the adversary (g, a • g, b • g), and check whether the adversary's output equals (a * b) • g.

DDH (Decisional Diffie-Hellman)

def DiffieHellman.DDHAdversary (_F G : Type) : Type

A DDH adversary receives (g, A, B, T) and guesses whether T = (a * b) • g (real) or T is a random group element (random). _F is a phantom type parameter for the scalar field, enabling Lean to infer F at call sites of ddhExp and related definitions.

def DiffieHellman.ddhExp {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] (g : G) (adversary : DDHAdversary F G) : ProbComp Bool

DDH experiment: sample random scalars a, b and a bit. If the bit is true, set c = a * b (the real DH scalar); otherwise sample c ← $ᵗ F independently. The adversary receives (g, a • g, b • g, c • g) and wins by guessing the bit.

All sampling is from the scalar field F, so the experiment is well-defined for any Module F G without requiring that g generates all of G.

noncomputable def DiffieHellman.ddhGuessAdvantage {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] (g : G) (adversary : DDHAdversary F G) : ℝ

DDH advantage: absolute distance from random guessing (1/2). Uses ℝ with absolute value rather than ℝ≥0∞ subtraction, which would silently saturate at zero for adversaries that guess the wrong bit more often than not.

DDH: Two-game formulation

def DiffieHellman.ddhExpReal {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] (g : G) (adversary : DDHAdversary F G) : ProbComp Bool

DDH real game: the adversary receives a genuine DH triple (g, a • g, b • g, (a * b) • g).

def DiffieHellman.ddhExpRand {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] (g : G) (adversary : DDHAdversary F G) : ProbComp Bool

DDH random game: the adversary receives (g, a • g, b • g, c • g) with independent c ← $ᵗ F.

noncomputable def DiffieHellman.ddhDistAdvantage {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] (g : G) (adversary : DDHAdversary F G) : ℝ

Two-game DDH advantage: |Pr[output 1 | real] - Pr[output 1 | random]|.

noncomputable def DiffieHellman.uniformDHTargetSuccessProb (F : Type) [Fintype F] : ℝ

Baseline success probability for matching an independently uniform DH target sampled from the scalar space and mapped into the subgroup generated by g.

Standard reductions among DLog / CDH / DDH

def DiffieHellman.cdhToDDHReduction {F G : Type} [DecidableEq G] (adversary : CDHAdversary F G) : DDHAdversary F G

Reduction from CDH solving to DDH distinguishing: compute a candidate DH share and compare it with the target group element. This is the concrete reduction underlying the hardness implication DDH ⇒ CDH.

def DiffieHellman.dlogToCDHReduction {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] (adversary : DLogAdversary F G) : CDHAdversary F G

Reduction from DLog solving to CDH solving: recover the two exponents separately and rebuild the shared DH value. This is the concrete reduction underlying CDH ⇒ DLog.

def DiffieHellman.dlogToDDHReduction {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [DecidableEq G] (adversary : DLogAdversary F G) : DDHAdversary F G

Direct DLog-to-DDH reduction obtained by composing the standard DLog-to-CDH and CDH-to-DDH reductions. This is the concrete reduction underlying DDH ⇒ DLog.

theorem DiffieHellman.ddhExp_probOutput_sub_half {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] (g : G) (adversary : DDHAdversary F G) : Pr[= true | ddhExp g adversary].toReal - 1 / 2 = (Pr[= true | ddhExpReal g adversary].toReal - Pr[= true | ddhExpRand g adversary].toReal) / 2

The single-game DDH decomposes: Pr[win] - 1/2 = (Pr[real=1] - Pr[rand=1]) / 2.

theorem DiffieHellman.ddhDistAdvantage_eq_two_mul_ddhGuessAdvantage {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] (g : G) (adversary : DDHAdversary F G) : ddhDistAdvantage g adversary = 2 * ddhGuessAdvantage g adversary

The two DDH advantage formulations are related by a factor of 2: ddhDistAdvantage = 2 * ddhGuessAdvantage.

theorem DiffieHellman.probOutput_ddhExpReal_cdhToDDHReduction_eq_cdhExp {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] [DecidableEq G] (g : G) (adversary : CDHAdversary F G) : Pr[= true | ddhExpReal g (cdhToDDHReduction adversary)] = Pr[= true | cdhExp g adversary]

In the real DDH game, the CDH-to-DDH reduction succeeds exactly when the underlying CDH adversary computed the correct shared DH value.

theorem DiffieHellman.probOutput_ddhExpRand_cdhToDDHReduction_eq_uniformScalar {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] [DecidableEq G] [Fintype F] (g : G) (hg : Function.Bijective fun (x : F) => x • g) (adversary : CDHAdversary F G) : Pr[= true | ddhExpRand g (cdhToDDHReduction adversary)] = (↑(Fintype.card F))⁻¹

In the random DDH game, the CDH-to-DDH reduction only matches the target with the uniform baseline probability. The bijectivity assumption identifies scalar samples with uniformly sampled group elements in the subgroup generated by g.

theorem DiffieHellman.cdhSuccess_toReal_le_uniform_add_ddhDistAdvantage {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType F] [DecidableEq G] [Fintype F] (g : G) (hg : Function.Bijective fun (x : F) => x • g) (adversary : CDHAdversary F G) : Pr[= true | cdhExp g adversary].toReal ≤ uniformDHTargetSuccessProb F + ddhDistAdvantage g (cdhToDDHReduction adversary)

Concrete form of the hardness implication DDH ⇒ CDH: a CDH solver can only beat the uniform DH-target baseline by the DDH distinguishing advantage of the associated adversary-map reduction.

theorem DiffieHellman.dlogSuccess_sq_le_cdhSuccess_dlogToCDHReduction {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [DecidableEq F] [SampleableType F] [DecidableEq G] (g : G) (adversary : DLogAdversary F G) : Pr[= true | dlogExp g adversary].toReal ^ 2 ≤ Pr[= true | cdhExp g (dlogToCDHReduction adversary)].toReal

Concrete form of the hardness implication CDH ⇒ DLog: if a DLog adversary succeeds with probability p, the induced CDH adversary succeeds with probability at least p^2.

theorem DiffieHellman.dlogSuccess_sq_le_uniform_add_ddhDistAdvantage {F : Type} [Field F] {G : Type} [AddCommGroup G] [Module F G] [DecidableEq F] [SampleableType F] [DecidableEq G] [Fintype F] (g : G) (hg : Function.Bijective fun (x : F) => x • g) (adversary : DLogAdversary F G) : Pr[= true | dlogExp g adversary].toReal ^ 2 ≤ uniformDHTargetSuccessProb F + ddhDistAdvantage g (dlogToDDHReduction adversary)

Concrete form of the hardness implication DDH ⇒ DLog, obtained by composing the previous two adversary-map reductions.

Generable relation for discrete log

def DiffieHellman.dlogGenerable {F : Type} [Field F] [SampleableType F] {G : Type} [AddCommGroup G] [Module F G] [DecidableEq G] (g : G) : GenerableRelation G F fun (pk : G) (sk : F) => decide (sk • g = pk)

The discrete log relation is generable by sampling sk ← $ᵗ F and returning (sk • g, sk).

Cyclic group instantiation helpers

def DiffieHellman.NondegenerateGenerator {G : Type} [AddCommGroup G] [Fintype G] (g : G) : Prop

A generator g is nondegenerate if fun a => a.val • g surjects onto G, ruling out the trivial case. Uses additive notation consistent with Module F G.

theorem DiffieHellman.NondegenerateGenerator.ne_zero {G : Type} [AddCommGroup G] [Fintype G] [Nontrivial G] {g : G} (hg : NondegenerateGenerator g) : g ≠ 0