Computational co-Diffie-Hellman (co-CDH) Assumption

The co-CDH assumption in bilinear groups: given (g₁, g₂, g₁^a, g₂^b), compute g₁^{ab}.

This is the standard hardness assumption underlying BLS signatures (Boneh-Lynn-Shacham 2004). It is equivalent to CDH in G₂ when the pairing exists, but stated in the Type III setting.

Main definitions

• CoCDH_Adversary — adversary that attempts to compute g₁^{ab}
• CoCDH_Game — the co-CDH game
• CoCDH_Advantage — probability of solving co-CDH
• CoCDHSecure — co-CDH hardness assumption

Cross-Validation

Property	This file	Paper
Challenge	(g₁^a, g₂^b)	BLS04 §3
Target	Compute g₁^{ab}	BLS04 §3
Group	PairingGroup P (Type-III)	Bilinear group (G₁, G₂, G_T)

Relationship to other assumptions:

• CDH in G₁ ⟹ co-CDH (co-CDH is weaker: adversary gets cross-group info)
• co-CDH is the standard BLS assumption; CDH in G₁ is sometimes used instead

References

• Boneh, Lynn, Shacham. Short Signatures from the Weil Pairing. J. Cryptology, 2004, §3.

co-CDH Game

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.CoCDH_Adversary (P : PairingGroup) : Type

co-CDH adversary: given (g₁^a, g₂^b), attempts to compute g₁^{ab}.

The adversary receives elements from both source groups and must produce an element of G₁.

Equations

• CatCrypt.Crypto.Assumptions.CoCDH_Adversary P = (CatCrypt.Crypto.PairingGroup.G₁ → CatCrypt.Crypto.PairingGroup.G₂ → CatCrypt.Core.SPComp CatCrypt.Crypto.PairingGroup.G₁)

noncomputable def CatCrypt.Crypto.Assumptions.CoCDH_Game (P : PairingGroup) (A : CoCDH_Adversary P) : Core.SPComp Bool

co-CDH game: sample a, b ← Zₚ; adversary receives (g₁^a, g₂^b) and wins if it outputs g₁^{ab}.

Returns true if the adversary's output equals g₁^{ab}.

Equations

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

noncomputable def CatCrypt.Crypto.Assumptions.CoCDH_Advantage (P : PairingGroup) (A : CoCDH_Adversary P) : ENNReal

co-CDH advantage: probability that the adversary computes g₁^{ab}.

Equations

• CatCrypt.Crypto.Assumptions.CoCDH_Advantage P A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.CoCDH_Game P A) CatCrypt.Core.Heap.empty

def CatCrypt.Crypto.Assumptions.CoCDHSecure (P : PairingGroup) (ε : ENNReal) : Prop

co-CDH hardness: all adversaries have bounded advantage.

Equations

• CatCrypt.Crypto.Assumptions.CoCDHSecure P ε = ∀ (A : CatCrypt.Crypto.Assumptions.CoCDH_Adversary P), CatCrypt.Crypto.Assumptions.CoCDH_Advantage P A ≤ ε