Discrete Logarithm Assumption

This file defines the DL (Discrete Logarithm) assumption for pairing groups. The DL assumption is used for the hiding property of KZG.

Main definitions

• DL_Game — The DL game in G₁: adversary receives g₁^x and must find x
• DL_Advantage — Advantage of an adversary in breaking DL

Cross-Validation

Property	This file	Textbook
Game structure	DL_Game	Boneh-Shoup Def. 10.4
Advantage	prTrue(DL_Game)	Pr[DLadv]
Group	PairingGroup P	Cyclic group of prime order

Equivalent formalizations:

• EasyCrypt: DLog theory in ec-toolbox/theories/crypto/CDH_DDH.ec
• CryptoVerif: DL(G, Z, g, exp, exp') macro

References

• Boneh & Shoup, A Graduate Course in Applied Cryptography, §10.5, Def. 10.4
• Katz & Lindell, Introduction to Modern Cryptography, §9.3
• [Palak, Haines, Formal Verification of KZG Polynomial Commitments, ESORICS 2025]

Discrete Logarithm Game

@[reducible, inline]

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

Type of DL adversary: receives a group element h = g₁^x, must output x

Equations

• CatCrypt.Crypto.Assumptions.DL_Adversary P = (CatCrypt.Crypto.PairingGroup.G₁ → CatCrypt.Core.SPComp (ZMod CatCrypt.Crypto.PairingGroup.p))

noncomputable def CatCrypt.Crypto.Assumptions.DL_Game (P : PairingGroup) (A : DL_Adversary P) : Core.SPComp Bool

The discrete log game in G₁: sample x, give g₁^x to adversary, check answer

Equations

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

noncomputable def CatCrypt.Crypto.Assumptions.DL_Advantage (P : PairingGroup) (A : DL_Adversary P) : ENNReal

Advantage of adversary A in breaking the DL assumption

Equations

• CatCrypt.Crypto.Assumptions.DL_Advantage P A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.DL_Game P A) CatCrypt.Core.Heap.empty