Fixed-first-coordinate DDH rerandomization and Multi-DDH

Fixed-first-coordinate rerandomization preserves the real DDH law and sends any non-DDH triple to the ideal pair law. Independent coordinate rerandomization gives the single-shared-secret case of Multi-DDH (I), with the exact exceptional-point loss 1 / q.

This is shared distributional support, not an efficient lazy-sampling reduction. The tuple wrapper samples every coordinate of its finite index type. Extracted from the reviewed Naor–Reingold source in PR #1103, authored by worker-jetski-cf53d356 (Gemini), with its mathematics unchanged.

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURerandomizeLaw_real: real fixed-coordinate law.
• Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURerandomizeLaw_ideal: non-DDH fixed-coordinate law.
• Cslib.Crypto.PrimeOrderGroupFamily.advantage_multiDDH_le: Multi-DDH loss for one shared secret.

References

• [BS23], Section 10.11, Exercises 10.8 and 10.11.

Fixed-$u$ DDH random self-reduction and Multi-DDH (I) (Exercises 10.8 & 10.11)

def Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURerandomize (F : PrimeOrderGroupFamily) (d : F.Desc) (u v w : F.Carrier d) (σ τ : ZMod (F.order d)) : F.Carrier d × F.Carrier d

Fixed-$u$ DDH rerandomization ([BS23], Section 10.11, Exercise 10.8, p. 425): given (u, v, w) and exponents σ, τ : ZMod (F.order d), output (v*, w*) = (σ • g + τ • v, σ • u + τ • w).

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURerandomize_smul_generator (F : PrimeOrderGroupFamily) (d : F.Desc) (α β γ σ τ : ZMod (F.order d)) : F.ddhFixedURerandomize d (α • F.generator d) (β • F.generator d) (γ • F.generator d) σ τ = ((σ + τ * β) • F.generator d, (α * (σ + τ * β) + τ * (γ - α * β)) • F.generator d)

Algebraic action of ddhFixedURerandomize on multiples of the generator: v* = (σ + τ * β) • g and w* = (α * (σ + τ * β) + τ * (γ - α * β)) • g.

def Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedUWordRerandomize (F : PrimeOrderGroupFamily) (d : F.Desc) (u v w : List Bool) (σ τ : ℕ) : List Bool × List Bool

Word-level fixed-$u$ DDH rerandomization on encoded group elements.

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedUWordRerandomize_encode (F : PrimeOrderGroupFamily) (d : F.Desc) (u v w : F.Carrier d) (σ τ : ℕ) : F.ddhFixedUWordRerandomize d (F.encode d u) (F.encode d v) (F.encode d w) σ τ = (F.encode d (F.ddhFixedURerandomize d u v w ↑σ ↑τ).1, F.encode d (F.ddhFixedURerandomize d u v w ↑σ ↑τ).2)

ddhFixedUWordRerandomize computes the encoded output of ddhFixedURerandomize.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_ddhFixedUWordRerandomize (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : F.Desc × List Bool × List Bool × List Bool × ℕ × ℕ) => F.ddhFixedUWordRerandomize input.1 input.2.1 input.2.2.1 input.2.2.2.1 input.2.2.2.2.1 input.2.2.2.2.2) (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

ddhFixedUWordRerandomize is computable in polynomial time.

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

The distribution of (v*, w*) obtained by drawing σ, τ : ZMod (F.order d) independently and uniformly in ddhFixedURerandomize ([BS23], Exercise 10.8, p. 425).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURealLaw (F : PrimeOrderGroupFamily) (d : F.Desc) (α : ZMod (F.order d)) : PMF (F.Carrier d × F.Carrier d)

The real DDH pair distribution (β • g, (α * β) • g) for a fixed first exponent α.

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

The ideal pair distribution (β • g, γ • g) on F.Carrier d × F.Carrier d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURerandomizeLaw_real (F : PrimeOrderGroupFamily) (d : F.Desc) (α β : ZMod (F.order d)) : F.ddhFixedURerandomizeLaw d (α • F.generator d) (β • F.generator d) ((α * β) • F.generator d) = F.ddhFixedURealLaw d α

Boneh–Shoup Exercise 10.8(a): if (u, v, w) = (α • g, β • g, (α * β) • g) is a DDH triple, then ddhFixedURerandomizeLaw produces ddhFixedURealLaw d α for every α, β.

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

Boneh–Shoup Exercise 10.8(b): if (u, v, w) = (α • g, β • g, γ • g) is a non-DDH triple (γ ≠ α * β), then ddhFixedURerandomizeLaw produces ddhFixedUIdealLaw d.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.multiDDHRealTupleLaw (F : PrimeOrderGroupFamily) (d : F.Desc) (ι : Type u_1) [Fintype ι] [DecidableEq ι] (α : ZMod (F.order d)) : PMF (ι → F.Carrier d × F.Carrier d)

The Multi-DDH (I) real tuple family i ↦ (B i • g, (α * B i) • g) for a fixed α and an index type ι ([BS23], Section 10.11, Exercise 10.11, p. 426).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.multiDDHIdealTupleLaw (F : PrimeOrderGroupFamily) (d : F.Desc) (ι : Type u_1) [Fintype ι] [DecidableEq ι] : PMF (ι → F.Carrier d × F.Carrier d)

The Multi-DDH (I) ideal tuple family i ↦ (B₀ i • g, B₁ i • g) for an index type ι ([BS23], Section 10.11, Exercise 10.11, p. 426).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.multiDDHRerandomizeLaw (F : PrimeOrderGroupFamily) (d : F.Desc) (ι : Type u_1) [Fintype ι] [DecidableEq ι] (u v w : F.Carrier d) : PMF (ι → F.Carrier d × F.Carrier d)

Multi-DDH (I) rerandomization ([BS23], Exercise 10.11, p. 426): given a single candidate DDH triple (u, v, w), draw independent (σ i, τ i) ← ZMod q × ZMod q for each i : ι and output i ↦ ddhFixedURerandomize d u v w (σ i) (τ i).

theorem Cslib.Crypto.PrimeOrderGroupFamily.multiDDHRerandomizeLaw_real (F : PrimeOrderGroupFamily) (d : F.Desc) (ι : Type u_1) [Fintype ι] [DecidableEq ι] (α β : ZMod (F.order d)) : F.multiDDHRerandomizeLaw d ι (α • F.generator d) (β • F.generator d) ((α * β) • F.generator d) = F.multiDDHRealTupleLaw d ι α

On any real DDH triple (α • g, β • g, (α * β) • g), multiDDHRerandomizeLaw produces multiDDHRealTupleLaw d ι α ([BS23], Exercise 10.11).

theorem Cslib.Crypto.PrimeOrderGroupFamily.multiDDHRerandomizeLaw_ideal (F : PrimeOrderGroupFamily) (d : F.Desc) (ι : Type u_1) [Fintype ι] [DecidableEq ι] {α β γ : ZMod (F.order d)} (hγ : γ ≠ α * β) : F.multiDDHRerandomizeLaw d ι (α • F.generator d) (β • F.generator d) (γ • F.generator d) = F.multiDDHIdealTupleLaw d ι

On any non-DDH triple (α • g, β • g, γ • g) with γ ≠ α * β, multiDDHRerandomizeLaw produces multiDDHIdealTupleLaw d ι ([BS23], Exercise 10.11).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_multiDDH_le (F : PrimeOrderGroupFamily) (d : F.Desc) (ι : Type u_1) [Fintype ι] [DecidableEq ι] (test : F.Carrier d → (ι → F.Carrier d × F.Carrier d) → PMF Bool) : Game.advantage ((Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (α : ZMod (F.order d)) => (F.multiDDHRealTupleLaw d ι α).bind (test (α • F.generator d))) ((Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (α : ZMod (F.order d)) => (F.multiDDHIdealTupleLaw d ι).bind (test (α • F.generator d))) ≤ Game.advantage ((F.ddhRealTupleLaw d).bind fun (t : F.Carrier d × F.Carrier d × F.Carrier d) => (F.multiDDHRerandomizeLaw d ι t.1 t.2.1 t.2.2).bind (test t.1)) ((F.ddhIdealTupleLaw d).bind fun (t : F.Carrier d × F.Carrier d × F.Carrier d) => (F.multiDDHRerandomizeLaw d ι t.1 t.2.1 t.2.2).bind (test t.1)) + (↑(F.order d))⁻¹

Boneh–Shoup Exercise 10.11 ($n = 1$ Multi-DDH (I), p. 426): for a single shared secret α, any finite index type ι (|ι| pairs), and any test test : F.Carrier d → (ι → F.Carrier d × F.Carrier d) → PMF Bool, the advantage between (α • g, multiDDHRealTupleLaw d ι α) and (α • g, multiDDHIdealTupleLaw d ι) is at most the DDH advantage of the rerandomizing wrapper multiDDHRerandomizeLaw (which samples |ι| pairs) plus (F.order d)⁻¹.