The Computational and Decisional Diffie–Hellman assumptions

Over a PrimeOrderGroupFamily, the Computational Diffie–Hellman (CDH) experiment ([BS23], Attack Game 10.5) draws a group description d from a setup law and two independent uniform exponents α, β : ZMod (F.order d), gives the adversary (d, encode (α • g), encode (β • g)), and accepts when the adversary outputs encode ((α * β) • g).

The Decisional Diffie–Hellman (DDH) experiment ([BS23], Attack Game 10.6) compares the real tuple (d, encode (α • g), encode (β • g), encode ((α * β) • g)) against the ideal tuple (d, encode (α • g), encode (β • g), encode (γ • g)) with an independent uniform γ.

We prove the implications DDH ⇒ CDH ⇒ DiscreteLog between the assumptions, the distributional rerandomisation lemma underlying the random self-reducibility of DDH ([BS23], Section 10.11, Exercises 10.8–10.9, pp. 425–426; ddhRerandomizeLaw_real and ddhRerandomizeLaw_ideal), its word-level and game-level consequences (encodeDDHRerandomize, ddhRerandomizeGame, ddhRerandomizeGame_real, ddhRerandomizeGame_ideal, advantage_ddhRerandomizeGame_eq, DDH.ddhRerandomizeGame), an original single-invocation worst-case-to-average-case DDH distinguishing reduction using ProbComp.sampleModNat (ddhSampleModExponents, ddhSelfReduceDistinguisher, ddhWorstCaseGame, advantage_ddhRerandomizeGame_ddhWorstCaseGame_le, advantage_ddhRealGame_le_ddhWorstCaseGame, ddh_of_worstCase), and the worst-case DDH decider of [BS23], Section 10.11, Exercise 10.10 (p. 426; ddhRealRefTuple, ddhIdealRefTuple, ddhAmplifiedDecider, isPPTOn_ddhAmplifiedDecider, ddhAmplifiedDecider_error_le_pow, negligible_ddhAmplifiedDecider_error), which amplifies an average-case distinguisher with inverse-polynomial advantage via repeated random self-reduction trials and a Chernoff/Hoeffding tail bound (ProbComp.countTrue_average_deviation_pow) so that it correctly decides every input tuple (α • g, β • g, γ • g) except with negligible error probability. The Diffie–Hellman assumptions are hypotheses, not theorems.

Main definitions

• Cslib.Crypto.PrimeOrderGroupFamily.cdhGame, Cslib.Crypto.PrimeOrderGroupFamily.CDH: the Computational Diffie–Hellman experiment and assumption.
• Cslib.Crypto.PrimeOrderGroupFamily.dlToCDHAdversary: the reduction from discrete logarithm to CDH.
• Cslib.Crypto.PrimeOrderGroupFamily.ddhRealGame, Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealGame, Cslib.Crypto.PrimeOrderGroupFamily.DDH: the real and ideal Decisional Diffie–Hellman experiments and assumption.
• Cslib.Crypto.PrimeOrderGroupFamily.cdhToDDHDistinguisher: the reduction from CDH to DDH.
• Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomize, Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeLaw, Cslib.Crypto.PrimeOrderGroupFamily.encodeDDHRerandomize, Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeGame: algebraic, word-level, and game-level DDH rerandomisation ([BS23], Exercises 10.8–10.9, pp. 425–426).
• Cslib.Crypto.PrimeOrderGroupFamily.sampleExp: approximate uniform exponent sampling modulo F.order d via ProbComp.sampleModNat with statistical distance at most 1 / 2 ^ n.
• Cslib.Crypto.PrimeOrderGroupFamily.ddhSampleModExponents, Cslib.Crypto.PrimeOrderGroupFamily.sampleModZModLaw, Cslib.Crypto.PrimeOrderGroupFamily.ddhSelfReduceDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.ddhWorstCaseGame: original single-invocation worst-case-to-average-case DDH distinguishing reduction.
• Cslib.Crypto.PrimeOrderGroupFamily.ddhRealRefTuple, Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealRefTuple, Cslib.Crypto.PrimeOrderGroupFamily.ddhAmplifiedDecider: reference DDH / non-DDH tuples and the Chernoff-amplified worst-case DDH decider ([BS23], Exercise 10.10, p. 426).

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.succProbability_discreteLogGame_le_cdhGame, Cslib.Crypto.PrimeOrderGroupFamily.CDH.discreteLog: CDH implies DiscreteLog.
• Cslib.Crypto.PrimeOrderGroupFamily.succProbability_cdhGame_le_advantage_ddh_add, Cslib.Crypto.PrimeOrderGroupFamily.DDH.cdh, Cslib.Crypto.PrimeOrderGroupFamily.DDH.discreteLog: DDH implies CDH and DiscreteLog when 1 / q is negligible.
• Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeLaw_real, Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeLaw_ideal: the distributional rerandomisation lemma for DDH tuples ([BS23], Exercises 10.8–10.9, pp. 425–426).
• Cslib.Crypto.PrimeOrderGroupFamily.encodeDDHRerandomize_encode, Cslib.Crypto.PrimeOrderGroupFamily.encodeDDHRerandomize_val, Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeDDHRerandomize, Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeGame_real, Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeGame_ideal, Cslib.Crypto.PrimeOrderGroupFamily.advantage_ddhRerandomizeGame_eq, Cslib.Crypto.PrimeOrderGroupFamily.DDH.ddhRerandomizeGame: word-level and game-level consequences of Exercises 10.8–10.9 (pp. 425–426).
• Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_sampleExp, Cslib.Crypto.PrimeOrderGroupFamily.advantage_bind_sampleExp_le, Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_ddhSampleModExponents, Cslib.Crypto.PrimeOrderGroupFamily.dist_sampleModZModLaw_le, Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_ddhSelfReduceDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.advantage_ddhRerandomizeGame_ddhWorstCaseGame_le, Cslib.Crypto.PrimeOrderGroupFamily.advantage_ddhRealGame_le_ddhWorstCaseGame, Cslib.Crypto.PrimeOrderGroupFamily.ddh_of_worstCase: original single-invocation worst-case-to-average-case DDH distinguishing reduction.
• Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_ddhAmplifiedDecider, Cslib.Crypto.PrimeOrderGroupFamily.ddhAmplifiedDecider_error_le_pow, Cslib.Crypto.PrimeOrderGroupFamily.ddhAmplifiedDecider_correct_ge_one_sub_pow, Cslib.Crypto.PrimeOrderGroupFamily.negligible_ddhAmplifiedDecider_error: worst-case DDH decision with negligible error from an average-case distinguisher with inverse-polynomial advantage ([BS23], Exercise 10.10, p. 426).

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 10.5 (Attack Games 10.5–10.6, pp. 409–410) and Section 10.11 (Exercises 10.7–10.10, pp. 425–426).

Computational Diffie–Hellman (CDH)

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.cdhGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : ℕ → F.Desc × List Bool × List Bool → ProbComp (List Bool)) (n : ℕ) : Game

The Computational Diffie–Hellman experiment ([BS23], Attack Game 10.5): draw a description d and independent uniform α, β : ZMod (F.order d), give the adversary the description and the encodings of α • g and β • g, and accept when it outputs the encoding of (α * β) • g.

def Cslib.Crypto.PrimeOrderGroupFamily.CDH (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) : Prop

The Computational Diffie–Hellman assumption for a family and a setup law: every uniform strict PPT adversary computes encode ((α * β) • g) from (d, encode (α • g), encode (β • g)) with negligible probability.

def Cslib.Crypto.PrimeOrderGroupFamily.dlToCDHAdversary (F : PrimeOrderGroupFamily) (adversary : ℕ → F.Desc × List Bool → ProbComp (List Bool)) (n : ℕ) (input : F.Desc × List Bool × List Bool) : ProbComp (List Bool)

Turn a discrete-logarithm adversary into a CDH adversary by running it on (d, encode (α • g)) to obtain a candidate exponent a and multiplying encode (β • g) by a.

theorem Cslib.Crypto.PrimeOrderGroupFamily.succProbability_discreteLogGame_le_cdhGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : ℕ → F.Desc × List Bool → ProbComp (List Bool)) (n : ℕ) : (F.discreteLogGame setup adversary n).succProbability ≤ (F.cdhGame setup (F.dlToCDHAdversary adversary) n).succProbability

Whenever the discrete-logarithm adversary recovers α, dlToCDHAdversary outputs the valid Diffie–Hellman shared element encode ((α * β) • g).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_dlToCDHAdversary (F : PrimeOrderGroupFamily) {adversary : ℕ → F.Desc × List Bool → ProbComp (List Bool)} (hA : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (input : ℕ × F.Desc × List Bool) => adversary input.1 input.2) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits fun (input : ℕ × F.Desc × List Bool × List Bool) => F.dlToCDHAdversary adversary input.1 input.2

The discrete-logarithm-to-CDH reduction is uniform strict PPT when the discrete-logarithm adversary is.

theorem Cslib.Crypto.PrimeOrderGroupFamily.CDH.discreteLog {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} (h : F.CDH setup) : F.DiscreteLog setup

CDH implies the discrete-logarithm assumption.

Decisional Diffie–Hellman (DDH)

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhRealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : Game

The real Decisional Diffie–Hellman experiment ([BS23], Attack Game 10.6): draw d and independent uniform α, β : ZMod (F.order d), and give the distinguisher (d, encode (α • g), encode (β • g), encode ((α * β) • g)).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : Game

The ideal Decisional Diffie–Hellman experiment ([BS23], Attack Game 10.6): draw d and independent uniform α, β, γ : ZMod (F.order d), and give the distinguisher (d, encode (α • g), encode (β • g), encode (γ • g)).

def Cslib.Crypto.PrimeOrderGroupFamily.DDH (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) : Prop

The Decisional Diffie–Hellman assumption for a family and a setup law: every uniform strict PPT distinguisher has negligible advantage between ddhRealGame and ddhIdealGame.

def Cslib.Crypto.PrimeOrderGroupFamily.cdhToDDHDistinguisher (F : PrimeOrderGroupFamily) (adversary : ℕ → F.Desc × List Bool × List Bool → ProbComp (List Bool)) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

Turn a CDH adversary into a DDH distinguisher by testing whether its candidate shared element equals the challenge third element.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRealGame_cdhToDDHDistinguisher (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : ℕ → F.Desc × List Bool × List Bool → ProbComp (List Bool)) (n : ℕ) : F.ddhRealGame setup (F.cdhToDDHDistinguisher adversary) n = F.cdhGame setup adversary n

In the real DDH game, cdhToDDHDistinguisher simulates the CDH game exactly.

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealGame_cdhToDDHDistinguisher_true_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : ℕ → F.Desc × List Bool × List Bool → ProbComp (List Bool)) (n m : ℕ) (hm : ∀ d ∈ (setup n).support, m ≤ F.order d) : (F.ddhIdealGame setup (F.cdhToDDHDistinguisher adversary) n) true ≤ (↑m)⁻¹

In the ideal DDH game, cdhToDDHDistinguisher succeeds with probability at most 1 / m whenever every supported group order is at least m.

theorem Cslib.Crypto.PrimeOrderGroupFamily.succProbability_cdhGame_le_advantage_ddh_add (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : ℕ → F.Desc × List Bool × List Bool → ProbComp (List Bool)) (n m : ℕ) (hm0 : 0 < m) (hm : ∀ d ∈ (setup n).support, m ≤ F.order d) : (F.cdhGame setup adversary n).succProbability ≤ (F.ddhRealGame setup (F.cdhToDDHDistinguisher adversary) n).advantage (F.ddhIdealGame setup (F.cdhToDDHDistinguisher adversary) n) + 1 / ↑m

Quantitative reduction from CDH to DDH: when every supported group at parameter n has order at least m > 0, any CDH adversary's success probability is at most the DDH distinguishing advantage of cdhToDDHDistinguisher plus 1 / m.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_cdhToDDHDistinguisher (F : PrimeOrderGroupFamily) {adversary : ℕ → F.Desc × List Bool × List Bool → ProbComp (List Bool)} (hA : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits fun (input : ℕ × F.Desc × List Bool × List Bool) => adversary input.1 input.2) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.cdhToDDHDistinguisher adversary input.1 input.2

The CDH-to-DDH reduction is uniform strict PPT when the CDH adversary is.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.cdh {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} (hDDH : F.DDH setup) {m : ℕ → ℕ} (hm0 : ∀ (n : ℕ), 0 < m n) (hm : ∀ (n : ℕ), ∀ d ∈ (setup n).support, m n ≤ F.order d) (hinv : Negligible fun (n : ℕ) => 1 / ↑(m n)) : F.CDH setup

DDH implies CDH when every supported group at parameter n has order at least m n > 0 and 1 / m n is negligible.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.discreteLog {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} (hDDH : F.DDH setup) {m : ℕ → ℕ} (hm0 : ∀ (n : ℕ), 0 < m n) (hm : ∀ (n : ℕ), ∀ d ∈ (setup n).support, m n ≤ F.order d) (hinv : Negligible fun (n : ℕ) => 1 / ↑(m n)) : F.DiscreteLog setup

DDH implies the discrete-logarithm assumption when every supported group at parameter n has order at least m n > 0 and 1 / m n is negligible.

Random self-reducibility of DDH

def Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomize (F : PrimeOrderGroupFamily) (d : F.Desc) (u v w : F.Carrier d) (r s₁ s₂ : ZMod (F.order d)) : F.Carrier d × F.Carrier d × F.Carrier d

Re-randomize a candidate DDH triple (u, v, w) in F.Carrier d using exponents r, s₁, s₂ : ZMod (F.order d).

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomize_smul_generator (F : PrimeOrderGroupFamily) (d : F.Desc) (α β γ r s₁ s₂ : ZMod (F.order d)) : F.ddhRerandomize d (α • F.generator d) (β • F.generator d) (γ • F.generator d) r s₁ s₂ = ((r * α + s₁) • F.generator d, (β + s₂) • F.generator d, ((r * α + s₁) * (β + s₂) + r * (γ - α * β)) • F.generator d)

Algebraic action of ddhRerandomize on multiples of the generator: a tuple error γ - α * β is scaled by r and added to the new Diffie–Hellman product (r * α + s₁) * (β + s₂).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeLaw (F : PrimeOrderGroupFamily) (d : F.Desc) (u v w : F.Carrier d) : PMF (F.Carrier d × F.Carrier d × F.Carrier d)

The re-randomized triple distribution obtained by drawing r, s₁, s₂ : ZMod (F.order d) independently and uniformly.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhRealTupleLaw (F : PrimeOrderGroupFamily) (d : F.Desc) : PMF (F.Carrier d × F.Carrier d × F.Carrier d)

The real DDH tuple distribution on F.Carrier d.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealTupleLaw (F : PrimeOrderGroupFamily) (d : F.Desc) : PMF (F.Carrier d × F.Carrier d × F.Carrier d)

The ideal DDH tuple distribution on F.Carrier d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeLaw_real (F : PrimeOrderGroupFamily) (d : F.Desc) (α β : ZMod (F.order d)) : F.ddhRerandomizeLaw d (α • F.generator d) (β • F.generator d) ((α * β) • F.generator d) = F.ddhRealTupleLaw d

Random self-reducibility of DDH (real case): re-randomizing any fixed real DDH tuple (α • g, β • g, (α * β) • g) yields the exact uniform real DDH tuple distribution.

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeLaw_ideal (F : PrimeOrderGroupFamily) (d : F.Desc) {α β γ : ZMod (F.order d)} (hγ : γ ≠ α * β) : F.ddhRerandomizeLaw d (α • F.generator d) (β • F.generator d) (γ • F.generator d) = F.ddhIdealTupleLaw d

Random self-reducibility of DDH (ideal case): re-randomizing any fixed non-DDH tuple (α • g, β • g, γ • g) with γ ≠ α * β yields the exact uniform ideal DDH tuple distribution.

Efficient word-level DDH random self-reduction

def Cslib.Crypto.PrimeOrderGroupFamily.encodeDDHRerandomize (F : PrimeOrderGroupFamily) (input : F.Desc × (List Bool × List Bool × List Bool) × ℕ × ℕ × ℕ) : List Bool × List Bool × List Bool

Word-level DDH tuple re-randomization ([BS23], Exercises 10.8–10.9, pp. 425–426): given (d, (u, v, w), r, s₁, s₂) on encoded group elements u, v, w : List Bool and natural-number exponents r, s₁, s₂ : ℕ, evaluate the encoded tuple corresponding to ddhRerandomize.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeDDHRerandomize_encode (F : PrimeOrderGroupFamily) (d : F.Desc) (u v w : F.Carrier d) (r s₁ s₂ : ℕ) : F.encodeDDHRerandomize (d, (F.encode d u, F.encode d v, F.encode d w), r, s₁, s₂) = have t := F.ddhRerandomize d u v w ↑r ↑s₁ ↑s₂; (F.encode d t.1, F.encode d t.2.1, F.encode d t.2.2)

encodeDDHRerandomize evaluates ddhRerandomize on encoded group elements.

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeDDHRerandomize_val (F : PrimeOrderGroupFamily) (d : F.Desc) (u v w : F.Carrier d) (r s₁ s₂ : ZMod (F.order d)) : F.encodeDDHRerandomize (d, (F.encode d u, F.encode d v, F.encode d w), r.val, s₁.val, s₂.val) = have t := F.ddhRerandomize d u v w r s₁ s₂; (F.encode d t.1, F.encode d t.2.1, F.encode d t.2.2)

Evaluating encodeDDHRerandomize at .val of exponents in ZMod (F.order d) agrees with ddhRerandomize.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeDDHRerandomize (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime F.encodeDDHRerandomize (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))

Word-level DDH tuple re-randomization is computable in polynomial time.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.sampleExp (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) : ProbComp ℕ

Sample one approximate uniform exponent modulo F.order d using n + |encNat (F.order d)| fair coins via ProbComp.sampleModNat, within statistical distance 1 / 2 ^ n of exact uniform on ZMod (F.order d).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_sampleExp (F : PrimeOrderGroupFamily) {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} {d : γ → F.Desc} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn F.encDesc) : Probability.IsPPTOn encIn Turing.MultiTapeTM.encNat fun (a : γ) => F.sampleExp (n a) (d a)

sampleExp is uniform strict PPT whenever n and d are computable in polynomial time.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_bind_sampleExp_le (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) (k : ZMod (F.order d) → Game) : Game.advantage ((F.sampleExp n d).eval.bind fun (s : ℕ) => k ↑s) ((Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind k) ≤ 1 / 2 ^ n

Replacing one sampleExp n d draw by an exact uniform draw on ZMod (F.order d) changes Game.advantage by at most 1 / 2 ^ n.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhSampleModExponents (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) : ProbComp (ℕ × ℕ × ℕ)

Sample three independent nearly-uniform exponents modulo F.order d at statistical distance at most 1 / 2 ^ n each using ProbComp.sampleModNat ((F.order d).size + n) (F.order d) (original).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_ddhSampleModExponents (F : PrimeOrderGroupFamily) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary F.encDesc) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) fun (input : ℕ × F.Desc) => F.ddhSampleModExponents input.1 input.2

ddhSampleModExponents is uniform strict PPT (original).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.sampleModZModLaw (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) : PMF (ZMod (F.order d))

Distribution of a single modular exponent sampled via ProbComp.sampleModNat at parameter n and group description d, projected to ZMod (F.order d) (original).

theorem Cslib.Crypto.PrimeOrderGroupFamily.dist_sampleModZModLaw_le (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) : dist (Probability.PMF.uniformOfFintype (ZMod (F.order d))) (F.sampleModZModLaw n d) ≤ 1 / 2 ^ n

Each modular exponent sampled by ProbComp.sampleModNat ((F.order d).size + n) (F.order d) is within statistical distance 1 / 2 ^ n of PMF.uniformOfFintype (ZMod (F.order d)) (original).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhSelfReduceDistinguisher (F : PrimeOrderGroupFamily) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

The single-invocation DDH random self-reduction distinguisher (original): given a DDH distinguisher distinguisher, re-randomize an input tuple (d, u, v, w) by sampling (r, s₁, s₂) ← F.ddhSampleModExponents n d, computing (u', v', w') = F.encodeDDHRerandomize (d, (u, v, w), r, s₁, s₂), and running distinguisher on (d, u', v', w').

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_ddhSelfReduceDistinguisher (F : PrimeOrderGroupFamily) {distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool} (hD : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => distinguisher input.1 input.2) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.ddhSelfReduceDistinguisher distinguisher input.1 input.2

ddhSelfReduceDistinguisher is uniform strict PPT whenever distinguisher is (original).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (tuple : (d : F.Desc) → F.Carrier d × F.Carrier d × F.Carrier d) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : Game

Game-level DDH tuple re-randomization experiment ([BS23], Exercises 10.8–10.9, pp. 425–426): draw d ← setup n and independent uniform r, s₁, s₂ : ZMod (F.order d), re-randomize the encoded tuple tuple d using encodeDDHRerandomize, and run distinguisher.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeGame_real (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (α β : (d : F.Desc) → ZMod (F.order d)) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : F.ddhRerandomizeGame setup (fun (d : F.Desc) => (α d • F.generator d, β d • F.generator d, (α d * β d) • F.generator d)) distinguisher n = F.ddhRealGame setup distinguisher n

Re-randomizing any family of real DDH tuples (α d • g, β d • g, (α d * β d) • g) with encodeDDHRerandomize produces the exact average-case ddhRealGame ([BS23], Exercises 10.8–10.9, pp. 425–426).

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRerandomizeGame_ideal (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (α β γ : (d : F.Desc) → ZMod (F.order d)) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) (hγ : ∀ d ∈ (setup n).support, γ d ≠ α d * β d) : F.ddhRerandomizeGame setup (fun (d : F.Desc) => (α d • F.generator d, β d • F.generator d, γ d • F.generator d)) distinguisher n = F.ddhIdealGame setup distinguisher n

Re-randomizing any family of non-DDH tuples (α d • g, β d • g, γ d • g) with γ d ≠ α d * β d on the support of setup n using encodeDDHRerandomize produces the exact average-case ddhIdealGame ([BS23], Exercises 10.8–10.9, pp. 425–426).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_ddhRerandomizeGame_eq (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (α β α' β' γ' : (d : F.Desc) → ZMod (F.order d)) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) (hγ' : ∀ d ∈ (setup n).support, γ' d ≠ α' d * β' d) : (F.ddhRerandomizeGame setup (fun (d : F.Desc) => (α d • F.generator d, β d • F.generator d, (α d * β d) • F.generator d)) distinguisher n).advantage (F.ddhRerandomizeGame setup (fun (d : F.Desc) => (α' d • F.generator d, β' d • F.generator d, γ' d • F.generator d)) distinguisher n) = (F.ddhRealGame setup distinguisher n).advantage (F.ddhIdealGame setup distinguisher n)

DDH rerandomization advantage identity ([BS23], Exercises 10.8–10.9, pp. 425–426): for any real DDH tuple family (α d, β d) and any non-DDH tuple family (α' d, β' d, γ' d) with γ' d ≠ α' d * β' d on the support of setup n, the distinguishing advantage after encodeDDHRerandomize equals the average-case DDH advantage.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.ddhRerandomizeGame {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} (hDDH : F.DDH setup) (α β α' β' γ' : (d : F.Desc) → ZMod (F.order d)) (hγ' : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ d ∈ (setup n).support, γ' d ≠ α' d * β' d) : Game.Indistinguishable (F.ddhRerandomizeGame setup fun (d : F.Desc) => (α d • F.generator d, β d • F.generator d, (α d * β d) • F.generator d)) (F.ddhRerandomizeGame setup fun (d : F.Desc) => (α' d • F.generator d, β' d • F.generator d, γ' d • F.generator d)) fun (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) => Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => distinguisher input.1 input.2

DDH rerandomization indistinguishability ([BS23], Exercises 10.8–10.9, pp. 425–426): under the average-case DDH assumption, no uniform strict PPT distinguisher can distinguish the exact re-randomization of any real DDH tuple family from the exact re-randomization of any non-DDH tuple family.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhWorstCaseGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (tuple : (d : F.Desc) → F.Carrier d × F.Carrier d × F.Carrier d) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : Game

The worst-case DDH experiment on a fixed tuple family tuple (original): draw d ← setup n and give the encoded tuple (d, encode (tuple d).1, encode (tuple d).2.1, encode (tuple d).2.2) directly to distinguisher.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_ddhRerandomizeGame_ddhWorstCaseGame_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (tuple : (d : F.Desc) → F.Carrier d × F.Carrier d × F.Carrier d) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : (F.ddhRerandomizeGame setup tuple distinguisher n).advantage (F.ddhWorstCaseGame setup tuple (F.ddhSelfReduceDistinguisher distinguisher) n) ≤ 3 / 2 ^ n

Statistical distance bound for ddhSelfReduceDistinguisher (original): replacing the three exact uniform ZMod (F.order d) exponents in ddhRerandomizeGame with ddhSampleModExponents n d changes the game output distribution by at most 3 / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_ddhRealGame_le_ddhWorstCaseGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (α β α' β' γ' : (d : F.Desc) → ZMod (F.order d)) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) (hγ' : ∀ d ∈ (setup n).support, γ' d ≠ α' d * β' d) : have tuple₀ := fun (d : F.Desc) => (α d • F.generator d, β d • F.generator d, (α d * β d) • F.generator d); have tuple₁ := fun (d : F.Desc) => (α' d • F.generator d, β' d • F.generator d, γ' d • F.generator d); (F.ddhRealGame setup distinguisher n).advantage (F.ddhIdealGame setup distinguisher n) ≤ (F.ddhWorstCaseGame setup tuple₀ (F.ddhSelfReduceDistinguisher distinguisher) n).advantage (F.ddhWorstCaseGame setup tuple₁ (F.ddhSelfReduceDistinguisher distinguisher) n) + 6 / 2 ^ n

Quantitative single-invocation worst-case-to-average-case DDH reduction (original): the average-case DDH advantage of distinguisher is at most the worst-case DDH advantage of ddhSelfReduceDistinguisher distinguisher plus 6 / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddh_of_worstCase (F : PrimeOrderGroupFamily) {setup : ℕ → PMF F.Desc} (α β α' β' γ' : (d : F.Desc) → ZMod (F.order d)) (hγ' : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ d ∈ (setup n).support, γ' d ≠ α' d * β' d) (hworst : Game.Indistinguishable (F.ddhWorstCaseGame setup fun (d : F.Desc) => (α d • F.generator d, β d • F.generator d, (α d * β d) • F.generator d)) (F.ddhWorstCaseGame setup fun (d : F.Desc) => (α' d • F.generator d, β' d • F.generator d, γ' d • F.generator d)) fun (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) => Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => distinguisher input.1 input.2) : F.DDH setup

Average-case DDH from worst-case DDH via ddhSelfReduceDistinguisher (original): if a worst-case real DDH tuple family is indistinguishable from a worst-case non-DDH tuple family for all uniform strict PPT distinguishers, then F.DDH setup holds.

Worst-case DDH decider via Chernoff amplification ([BS23], Exercise 10.10)

def Cslib.Crypto.PrimeOrderGroupFamily.ddhRealRefTuple (F : PrimeOrderGroupFamily) (d : F.Desc) : List Bool × List Bool × List Bool

Canonical encoded real DDH tuple (0 • g, 0 • g, (0 * 0) • g) for group description d, computed in polynomial time via F.smul (d, 0, F.encode d (F.generator d)) ([BS23], Section 10.11, Exercise 10.10, p. 426).

def Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealRefTuple (F : PrimeOrderGroupFamily) (d : F.Desc) : List Bool × List Bool × List Bool

Canonical encoded non-DDH tuple (0 • g, 0 • g, 1 • g) for group description d (since 1 ≠ 0 * 0 in ZMod (F.order d) for prime F.order d; [BS23], Section 10.11, Exercise 10.10, p. 426).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRealRefTuple_eq_encode (F : PrimeOrderGroupFamily) (d : F.Desc) : F.ddhRealRefTuple d = (F.encode d (0 • F.generator d), F.encode d (0 • F.generator d), F.encode d ((0 * 0) • F.generator d))

ddhRealRefTuple equals the encoded tuple ((0 : ZMod q) • g, (0 : ZMod q) • g, ((0 : ZMod q) * 0) • g).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealRefTuple_eq_encode (F : PrimeOrderGroupFamily) (d : F.Desc) : F.ddhIdealRefTuple d = (F.encode d (0 • F.generator d), F.encode d (0 • F.generator d), F.encode d (1 • F.generator d))

ddhIdealRefTuple equals the encoded tuple ((0 : ZMod q) • g, (0 : ZMod q) • g, (1 : ZMod q) • g).

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_ddhRealRefTuple (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime F.ddhRealRefTuple F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))

ddhRealRefTuple is computable in polynomial time.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_ddhIdealRefTuple (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime F.ddhIdealRefTuple F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))

ddhIdealRefTuple is computable in polynomial time.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhWorstCaseGame_pure (F : PrimeOrderGroupFamily) (d : F.Desc) (tuple : (d : F.Desc) → F.Carrier d × F.Carrier d × F.Carrier d) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : F.ddhWorstCaseGame (fun (x : ℕ) => PMF.pure d) tuple distinguisher n = (distinguisher n (d, F.encode d (tuple d).1, F.encode d (tuple d).2.1, F.encode d (tuple d).2.2)).eval

On a deterministic group setup fun _ => PMF.pure d, ddhWorstCaseGame evaluates distinguisher directly on (d, encode (tuple d)).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_ddhRealGame_pure_ddhSelfReduceDistinguisher_le (F : PrimeOrderGroupFamily) (d : F.Desc) (α β : ZMod (F.order d)) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : (F.ddhRealGame (fun (x : ℕ) => PMF.pure d) distinguisher n).advantage (F.ddhSelfReduceDistinguisher distinguisher n (d, F.encode d (α • F.generator d), F.encode d (β • F.generator d), F.encode d ((α * β) • F.generator d))).eval ≤ 3 / 2 ^ n

Single-trial real DDH proximity: on any fixed group d and any real DDH triple (α • g, β • g, (α * β) • g), the acceptance probability of ddhSelfReduceDistinguisher differs from the average-case ddhRealGame (fun _ => PMF.pure d) acceptance probability by at most 3 / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_ddhIdealGame_pure_ddhSelfReduceDistinguisher_le (F : PrimeOrderGroupFamily) (d : F.Desc) {α β γ : ZMod (F.order d)} (hγ : γ ≠ α * β) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : (F.ddhIdealGame (fun (x : ℕ) => PMF.pure d) distinguisher n).advantage (F.ddhSelfReduceDistinguisher distinguisher n (d, F.encode d (α • F.generator d), F.encode d (β • F.generator d), F.encode d (γ • F.generator d))).eval ≤ 3 / 2 ^ n

Single-trial non-DDH proximity: on any fixed group d and any non-DDH triple (α • g, β • g, γ • g) with γ ≠ α * β, the acceptance probability of ddhSelfReduceDistinguisher differs from the average-case ddhIdealGame (fun _ => PMF.pure d) acceptance probability by at most 3 / 2 ^ n.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhAmplifiedDecider (F : PrimeOrderGroupFamily) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (invEps : ℕ → ℕ) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

Chernoff-amplified worst-case DDH decider ([BS23], Section 10.11, Exercise 10.10, p. 426): given an average-case DDH distinguisher distinguisher and an inverse-advantage bound invEps : ℕ → ℕ, perform N = (n + 3) * (7 * invEps n) ^ 2 independent trials of ddhSelfReduceDistinguisher on the input tuple (d, u, v, w), on the reference DH tuple ddhRealRefTuple d, and on the reference non-DH tuple ddhIdealRefTuple d, and accept iff the empirical count cIn is at least as close to cReal as to cIdeal.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_ddhAmplifiedDecider (F : PrimeOrderGroupFamily) {distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool} (hD : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => distinguisher input.1 input.2) {invEps : ℕ → ℕ} (hinvEps : Turing.MultiTapeTM.ComputableInPolyTime invEps Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.ddhAmplifiedDecider distinguisher invEps input.1 input.2

ddhAmplifiedDecider is uniform strict PPT whenever distinguisher is uniform strict PPT and invEps is computable in polynomial time in unary ([BS23], Exercise 10.10, p. 426).

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhAmplifiedDecider_error_le_pow (F : PrimeOrderGroupFamily) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (invEps : ℕ → ℕ) (n : ℕ) (d : F.Desc) (α β γ : ZMod (F.order d)) (hpos : 0 < invEps n) (hadv : 1 / ↑(invEps n) ≤ ↑((F.ddhRealGame (fun (x : ℕ) => PMF.pure d) distinguisher n).advantage (F.ddhIdealGame (fun (x : ℕ) => PMF.pure d) distinguisher n))) (hmod : 3 / 2 ^ n ≤ 1 / (12 * ↑(invEps n))) : ((F.ddhAmplifiedDecider distinguisher invEps n (d, F.encode d (α • F.generator d), F.encode d (β • F.generator d), F.encode d (γ • F.generator d))).eval.toOuterMeasure {b : Bool | b ≠ decide (γ = α * β)}).toReal ≤ (1 / 2) ^ n

Quantitative worst-case DDH decision bound ([BS23], Section 10.11, Exercise 10.10, p. 426): if distinguisher n has average-case DDH advantage at least 1 / invEps n on group d and the modular-sampling bias satisfies 3 / 2 ^ n ≤ 1 / (12 * invEps n), then for every triple (α • g, β • g, γ • g) over d, ddhAmplifiedDecider outputs an answer different from decide (γ = α * β) with probability at most (1 / 2) ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhAmplifiedDecider_correct_ge_one_sub_pow (F : PrimeOrderGroupFamily) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (invEps : ℕ → ℕ) (n : ℕ) (d : F.Desc) (α β γ : ZMod (F.order d)) (hpos : 0 < invEps n) (hadv : 1 / ↑(invEps n) ≤ ↑((F.ddhRealGame (fun (x : ℕ) => PMF.pure d) distinguisher n).advantage (F.ddhIdealGame (fun (x : ℕ) => PMF.pure d) distinguisher n))) (hmod : 3 / 2 ^ n ≤ 1 / (12 * ↑(invEps n))) : 1 - (1 / 2) ^ n ≤ ((F.ddhAmplifiedDecider distinguisher invEps n (d, F.encode d (α • F.generator d), F.encode d (β • F.generator d), F.encode d (γ • F.generator d))).eval (decide (γ = α * β))).toReal

Directional correctness of ddhAmplifiedDecider ([BS23], Section 10.11, Exercise 10.10, p. 426): under the hypotheses of ddhAmplifiedDecider_error_le_pow, on every triple (α • g, β • g, γ • g) over d, ddhAmplifiedDecider outputs the correct decision decide (γ = α * β) with probability at least 1 - (1 / 2) ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.negligible_ddhAmplifiedDecider_error (F : PrimeOrderGroupFamily) {distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool} {invEps : ℕ → ℕ} (hinvEps : Turing.MultiTapeTM.ComputableInPolyTime invEps Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (d : ℕ → F.Desc) (α β γ : (n : ℕ) → ZMod (F.order (d n))) (hpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < invEps n) (hadv : ∀ᶠ (n : ℕ) in Filter.atTop, 1 / ↑(invEps n) ≤ ↑((F.ddhRealGame (fun (x : ℕ) => PMF.pure (d n)) distinguisher n).advantage (F.ddhIdealGame (fun (x : ℕ) => PMF.pure (d n)) distinguisher n))) : Negligible fun (n : ℕ) => ((F.ddhAmplifiedDecider distinguisher invEps n (d n, F.encode (d n) (α n • F.generator (d n)), F.encode (d n) (β n • F.generator (d n)), F.encode (d n) (γ n • F.generator (d n)))).eval.toOuterMeasure {b : Bool | b ≠ decide (γ n = α n * β n)}).toNNReal

Boneh–Shoup Exercise 10.10 (Worst-case DDH decider with negligible error, p. 426): if invEps is computable in polynomial time in unary and distinguisher has average-case DDH advantage at least 1 / invEps n on d n eventually, then for every worst-case sequence of input tuples (d n, α n, β n, γ n), ddhAmplifiedDecider decides whether γ n = α n * β n with negligible error probability.