t-Strong Diffie-Hellman Assumption

This file defines the t-SDH (t-Strong Diffie-Hellman) assumption, which is the core hardness assumption for KZG polynomial commitments.

Main definitions

• tSDH_Game — The t-SDH game: adversary receives SRS [g₁, g₁^α, ..., g₁^(αᵗ)] and must output (c, g₁^(1/(α+c))) for some c ∈ Zₚ
• tSDH_Advantage — Advantage of an adversary in breaking t-SDH

Cross-Validation

Property	This file	Paper
Challenge	srs₁ α t = [g₁^{α⁰}, ..., g₁^{αᵗ}]	KZG §3.1
Verification	e(h, g₂^{α+c}) = e(g₁, g₂)	Boneh-Boyen Def. 3
Advantage	prTrue(tSDH_Game)	Pr[t-SDH]

Equivalent formalizations:

• EasyCrypt: SDH theory in KZG formalization (Palak-Haines)

References

• [Boneh, Boyen, Short Signatures Without Random Oracles, EUROCRYPT 2004, Def. 3]
• [Kate, Zaverucha, Goldberg, Constant-Size Commitments to Polynomials, ASIACRYPT 2010, §3.1]

t-SDH Game

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.tSDH_Adversary (P : PairingGroup) (t : ℕ) : Type

Type of t-SDH adversary: receives SRS of size t+1, outputs (c, h) where h should equal g₁^(1/(α+c)).

Equations

• CatCrypt.Crypto.Assumptions.tSDH_Adversary P t = ((Fin (t + 1) → CatCrypt.Crypto.PairingGroup.G₁) → CatCrypt.Core.SPComp (ZMod CatCrypt.Crypto.PairingGroup.p × CatCrypt.Crypto.PairingGroup.G₁))

noncomputable def CatCrypt.Crypto.Assumptions.tSDH_Game (P : PairingGroup) (t : ℕ) (A : tSDH_Adversary P t) : Core.SPComp Bool

The t-SDH game: sample secret α, compute SRS, run adversary, check solution.

The adversary wins if it outputs (c, h) such that h = g₁^(1/(α+c)), which we verify using the pairing: e(h, g₂^α · g₂^c) = e(g₁, g₂).

Equations

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

noncomputable def CatCrypt.Crypto.Assumptions.tSDH_Advantage (P : PairingGroup) (t : ℕ) (A : tSDH_Adversary P t) : ENNReal

Advantage of adversary A in breaking the t-SDH assumption

Equations

• CatCrypt.Crypto.Assumptions.tSDH_Advantage P t A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.tSDH_Game P t A) CatCrypt.Core.Heap.empty

Extended t-SDH Game (with verification key)

The standard formulation (Kate et al., Boneh-Boyen) provides the adversary with both the G₁ SRS and the G₂ verification key vk = (g₂, g₂^α).

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.tSDH_Adversary_ext (P : PairingGroup) (t : ℕ) : Type

Extended t-SDH adversary: receives both SRS in G₁ and verification key in G₂.

Equations

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

noncomputable def CatCrypt.Crypto.Assumptions.tSDH_Game_ext (P : PairingGroup) (t : ℕ) (A : tSDH_Adversary_ext P t) : Core.SPComp Bool

Extended t-SDH game: adversary receives pk and vk = (g₂, g₂^α).

Equations

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

noncomputable def CatCrypt.Crypto.Assumptions.tSDH_Advantage_ext (P : PairingGroup) (t : ℕ) (A : tSDH_Adversary_ext P t) : ENNReal

Advantage in the extended t-SDH game.

Equations

• CatCrypt.Crypto.Assumptions.tSDH_Advantage_ext P t A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.tSDH_Game_ext P t A) CatCrypt.Core.Heap.empty

theorem CatCrypt.Crypto.Assumptions.tSDH_Advantage_eq_ext (P : PairingGroup) (t : ℕ) (A : tSDH_Adversary P t) : tSDH_Advantage P t A = tSDH_Advantage_ext P t fun (pk : Fin (t + 1) → PairingGroup.G₁) (_vk : PairingGroup.G₂ × PairingGroup.G₂) => A pk

Any basic t-SDH adversary can be lifted to an extended one (ignoring vk). The advantage is preserved.

Useful lemma: SRS evaluation equals polynomial commitment

theorem CatCrypt.Crypto.Assumptions.srs₁_eq (P : PairingGroup) (α : ZMod PairingGroup.p) (t : ℕ) (i : Fin (t + 1)) : PairingGroup.srs₁ α t i = PairingGroup.zpowZMod₁ PairingGroup.g₁ (α ^ ↑i)

The SRS at position i is g₁^(αⁱ)