q-Strong Diffie-Hellman (q-SDH) Assumption

The q-SDH assumption is the core hardness assumption for BBS/BBS+ signatures and anonymous credentials. It generalizes the strong DH assumption to a setting where the adversary receives multiple powers of a secret exponent.

q-SDH Game

Given a group of prime order p with generator g:

• The challenger samples a secret x ← Zₚ
• The adversary receives (g, g^x, g^{x²}, ..., g^{x^q})
• The adversary must output (c, g^{1/(x+c)}) for some c ∈ Zₚ \ {-x}

Main definitions

• qSDH_Group — abstract group supporting q-SDH
• qSDH_Game — the q-SDH game
• qSDH_Advantage — advantage of an adversary

Cross-Validation

Property	This file	Paper
Challenge	qSDH_challenge x q = (g, g^x, ..., g^{x^q})	BB04 Def. 3
Verification	h^{x+c} = g	BB04 Def. 3
Group	qSDH_Group (abstract cyclic group)	Type-III pairing G₁

Relationship to t-SDH (Assumptions/tSDH.lean):

• tSDH uses PairingGroup with bilinear pairing verification
• qSDH uses an abstract group with exponentiation-based verification
• Both capture the same hardness assumption in different algebraic settings

Equivalent formalizations:

• EasyCrypt: SDH theory (Tessaro-Zhu BBS formalization)

References

• [Boneh, Boyen. Short Signatures Without Random Oracles. EUROCRYPT 2004, Def. 3]
• [Tessaro, Zhu. Revisiting BBS Signatures. EUROCRYPT 2023]

q-SDH Group Definition

structure CatCrypt.Crypto.Assumptions.qSDH_Group : Type 1

Abstract group supporting the q-SDH assumption.

This captures a cyclic group of prime order where exponentiation and the q-SDH challenge are well-defined.

For BBS signatures, this is a Type-III pairing group, but we abstract over the pairing structure since q-SDH only needs the G₁ component.

• G : Type

  Group element type

• Scalar : Type

  Scalar/exponent type (≅ Zₚ)

• gen : self.G

  Generator

• smul : self.Scalar → self.G → self.G

  Scalar multiplication (exponentiation): g^a

• scalarAdd : self.Scalar → self.Scalar → self.Scalar

  Scalar addition

• scalarMul : self.Scalar → self.Scalar → self.Scalar

  Scalar multiplication

• scalarInv : self.Scalar → self.Scalar

  Scalar inverse (for 1/(x+c))

• scalarZero : self.Scalar

  Zero scalar

• scalarOne : self.Scalar

  One scalar (multiplicative identity, for x^0 = 1)

• decG : DecidableEq self.G

  Decidable equality on G

• decScalar : DecidableEq self.Scalar

  Decidable equality on Scalar

• finG : Fintype self.G

  Group is finite

• neG : Nonempty self.G

  Group is nonempty

• finScalar : Fintype self.Scalar

  Scalar is finite (for uniform sampling)

• neScalar : Nonempty self.Scalar

  Scalar is nonempty

def CatCrypt.Crypto.Assumptions.scalarPow (QG : qSDH_Group) (x : QG.Scalar) : ℕ → QG.Scalar

Iterated scalar multiplication: compute x^i in the scalar field.

Equations

• CatCrypt.Crypto.Assumptions.scalarPow QG x 0 = QG.scalarOne
• CatCrypt.Crypto.Assumptions.scalarPow QG x n.succ = QG.scalarMul x (CatCrypt.Crypto.Assumptions.scalarPow QG x n)

def CatCrypt.Crypto.Assumptions.qSDH_challenge (QG : qSDH_Group) (x : QG.Scalar) (q : ℕ) : Fin (q + 1) → QG.G

The q-SDH challenge: (g, g^x, g^{x²}, ..., g^{x^q}).

Given secret x, compute the tuple of q+1 group elements.

Equations

• CatCrypt.Crypto.Assumptions.qSDH_challenge QG x q i = QG.smul (CatCrypt.Crypto.Assumptions.scalarPow QG x ↑i) QG.gen

q-SDH Game

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.qSDH_Adversary (QG : qSDH_Group) (q : ℕ) : Type

Type of q-SDH adversary: receives the challenge tuple, outputs (c, h) where h should equal g^{1/(x+c)}.

Equations

• CatCrypt.Crypto.Assumptions.qSDH_Adversary QG q = ((Fin (q + 1) → QG.G) → CatCrypt.Core.SPComp (QG.Scalar × QG.G))

noncomputable def CatCrypt.Crypto.Assumptions.qSDH_Game (QG : qSDH_Group) (q : ℕ) (A : qSDH_Adversary QG q) : Core.SPComp Bool

The q-SDH game.

1. Sample secret x ← Zₚ
2. Compute challenge (g, g^x, ..., g^{x^q})
3. Adversary outputs (c, h)
4. Verify: h = g^{1/(x+c)}, i.e., h^{x+c} = g

We verify by checking smul (scalarAdd x c) h = gen.

Equations

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

noncomputable def CatCrypt.Crypto.Assumptions.qSDH_Advantage (QG : qSDH_Group) (q : ℕ) (A : qSDH_Adversary QG q) : ENNReal

Advantage of adversary A in breaking the q-SDH assumption.

Equations

• CatCrypt.Crypto.Assumptions.qSDH_Advantage QG q A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.qSDH_Game QG q A) CatCrypt.Core.Heap.empty

IsPure

theorem CatCrypt.Crypto.Assumptions.qSDH_Game_isPure (QG : qSDH_Group) (q : ℕ) (A : qSDH_Adversary QG q) (hA : ∀ (ch : Fin (q + 1) → QG.G), (A ch).IsPure) : (qSDH_Game QG q A).IsPure