Algebraic Group Model (AGM)

This file formalizes the Algebraic Group Model, where adversaries must provide algebraic representations of all group elements they output.

Main definitions

• AGMRepr — a group element of G₁ paired with a claimed exponent vector
• AGMRepr.Valid — the representation equation against a given basis
• AGMRepr.ofCoeffs — the element computed from a basis and an exponent vector
• AGMAdversary — an adversary that receives the SRS and outputs representations

Main results

• AGMRepr.ofCoeffs_valid — the computed element satisfies the equation
• AGMRepr.element_eq_of_valid_srs₁ — against the KZG SRS, a valid representation is g₁ ^ᵍ φ(α) for the extracted polynomial φ

Overview

In the AGM, any group element output by the adversary must be accompanied by a vector of exponents showing how it was computed from the input group elements. For KZG, the input is the SRS [g₁, g₁^α, ..., g₁^(αᵗ)], and the output commitment C comes with [c₀, ..., cₜ]. A representation is valid for the SRS srs when C = ∏ srs[i]^cᵢ. Validity is relative to the SRS the game supplies: the game checks it and counts an invalid representation as a loss for the adversary (Fuchsbauer–Kiltz–Loss, Definition 2.1).

A valid representation means the adversary "knows" a polynomial φ(X) = ∑ cᵢ Xⁱ such that C = g₁^(φ(α)), enabling knowledge extraction.

References

• [Fuchsbauer, Kiltz, Loss, The Algebraic Group Model and its Applications, CRYPTO 2018]
• [Rothmann, Kreuzer — Algebraic_Group_Model.thy in Isabelle]
• [ArkLib — AGM/Basic.lean]

AGM Representation

structure CatCrypt.Crypto.AGMRepr (P : PairingGroup) (t : ℕ) : Type

A group element of G₁ together with a claimed algebraic representation with respect to a basis of size t + 1: a vector of exponents [c₀, ..., cₜ] in ZMod p. Whether the exponents represent the element depends on the basis and is the proposition AGMRepr.Valid.

• coeffs : Fin (t + 1) → ZMod PairingGroup.p

  The exponent vector

• element : PairingGroup.G₁

  The represented group element

def CatCrypt.Crypto.AGMRepr.Valid (P : PairingGroup) (t : ℕ) (repr : AGMRepr P t) (pk : Fin (t + 1) → PairingGroup.G₁) : Prop

The representation equation against the basis pk: element = ∏ᵢ pk[i]^coeffs[i].

Equations

• CatCrypt.Crypto.AGMRepr.Valid P t repr pk = (repr.element = ∏ i : Fin (t + 1), CatCrypt.Crypto.PairingGroup.zpowZMod₁ (pk i) (repr.coeffs i))

@[instance_reducible]

noncomputable instance CatCrypt.Crypto.AGMRepr.instDecidableValid (P : PairingGroup) (t : ℕ) (repr : AGMRepr P t) (pk : Fin (t + 1) → PairingGroup.G₁) : Decidable (Valid P t repr pk)

Equations

• CatCrypt.Crypto.AGMRepr.instDecidableValid P t repr pk = CatCrypt.Crypto.AGMRepr.instDecidableValid._aux_1 P t repr pk

noncomputable def CatCrypt.Crypto.AGMRepr.ofCoeffs (P : PairingGroup) (t : ℕ) (pk : Fin (t + 1) → PairingGroup.G₁) (coeffs : Fin (t + 1) → ZMod PairingGroup.p) : AGMRepr P t

The representation whose element is computed from the basis pk and the exponent vector coeffs.

Equations

• CatCrypt.Crypto.AGMRepr.ofCoeffs P t pk coeffs = { coeffs := coeffs, element := ∏ i : Fin (t + 1), CatCrypt.Crypto.PairingGroup.zpowZMod₁ (pk i) (coeffs i) }

theorem CatCrypt.Crypto.AGMRepr.ofCoeffs_valid (P : PairingGroup) (t : ℕ) (pk : Fin (t + 1) → PairingGroup.G₁) (coeffs : Fin (t + 1) → ZMod PairingGroup.p) : Valid P t (ofCoeffs P t pk coeffs) pk

A representation computed from a basis is valid for that basis.

noncomputable def CatCrypt.Crypto.AGMRepr.toPoly (P : PairingGroup) (t : ℕ) (repr : AGMRepr P t) : Polynomial (ZMod PairingGroup.p)

Extract the polynomial from an AGM representation. The polynomial is φ(X) = ∑ᵢ cᵢ · Xⁱ where cᵢ are the coefficients.

Equations

• CatCrypt.Crypto.AGMRepr.toPoly P t repr = ∑ i : Fin (t + 1), Polynomial.C (repr.coeffs i) * Polynomial.X ^ ↑i

Extracted Polynomial Properties

theorem CatCrypt.Crypto.AGMRepr.toPoly_coeff (P : PairingGroup) (t : ℕ) (repr : AGMRepr P t) (j : Fin (t + 1)) : (toPoly P t repr).coeff ↑j = repr.coeffs j

Coefficient of toPoly at position j matches the AGM coefficient.

theorem CatCrypt.Crypto.AGMRepr.toPoly_natDegree_le (P : PairingGroup) (t : ℕ) (repr : AGMRepr P t) : (toPoly P t repr).natDegree ≤ t

The extracted polynomial has degree at most t.

theorem CatCrypt.Crypto.AGMRepr.toPoly_ofCoeffs_coeff (P : PairingGroup) (t : ℕ) (pk : Fin (t + 1) → PairingGroup.G₁) (φ : Polynomial (ZMod PairingGroup.p)) (hdeg : φ.natDegree ≤ t) : toPoly P t (ofCoeffs P t pk fun (i : Fin (t + 1)) => φ.coeff ↑i) = φ

The representation whose exponents are the first t + 1 coefficients of φ extracts to φ when φ has degree at most t.

theorem CatCrypt.Crypto.AGMRepr.element_eq_of_valid_srs₁ (P : PairingGroup) (t : ℕ) (α : ZMod PairingGroup.p) (repr : AGMRepr P t) (hvalid : Valid P t repr (PairingGroup.srs₁ α t)) : repr.element = PairingGroup.zpowZMod₁ PairingGroup.g₁ (Polynomial.eval α (toPoly P t repr))

A representation valid for the KZG SRS srs₁ α t has element g₁ ^ᵍ φ(α), where φ is the extracted polynomial.

AGM Adversary

structure CatCrypt.Crypto.AGMAdversary (P : PairingGroup) (t : ℕ) : Type

An AGM adversary for KZG.

In the AGM, the adversary receives the SRS and outputs a commitment C together with an algebraic representation of C in terms of the SRS, an evaluation point, a claimed value, and a witness with its representation. The game that runs the adversary checks the representations against the SRS it supplied.

• run : (Fin (t + 1) → PairingGroup.G₁) → Core.SPComp (AGMRepr P t × ZMod PairingGroup.p × ZMod PairingGroup.p × AGMRepr P t)

  The adversary's computation: given the SRS, output (C_repr, z, y, w_repr), the commitment representation, the evaluation point, the claimed value and the witness representation.