KZG Knowledge Soundness in the AGM #
This file proves knowledge soundness of KZG in the Algebraic Group Model: any adversary that produces a valid evaluation proof must "know" the committed polynomial (in the AGM sense).
Main theorems #
KZG_knowledge_sound— the knowledge soundness game is bounded by(t + 1)times the t-SDH advantage of the reductionks_to_tSDHhonestAGMOutput_checks— the honest committer's output passes the game's representation and pairing checks, with representations extracting to the committed polynomial and its witness polynomial (honestAGMOutput_toPoly)
Proof outline #
In the AGM, the adversary outputs:
- Commitment C with representation
[c₀, ..., cₜ](implying polynomial φ) - Evaluation proof (z, y, w) with representation
[d₀, ..., dₜ](implying polynomial ψ)
The game checks both representations against the SRS it sampled; an output
with an invalid representation loses. For valid representations,
C = g₁^(φ(α)) and w = g₁^(ψ(α)), and the pairing verification equation forces:
φ(α) - y = ψ(α) · (α - z) in the exponent
In the AGM, this is a polynomial identity φ(X) - y = ψ(X) · (X - z) modulo
a polynomial that vanishes at α. If this identity doesn't hold as polynomials,
we can extract a nontrivial polynomial with α as a root, which breaks t-SDH.
References #
- [Rothmann, Kreuzer — KZG_Knowledge_Soundness.thy in Isabelle]
- [Kate, Zaverucha, Goldberg, 2010 — Theorem 2 (informal)]
Full Knowledge Soundness Game #
Knowledge soundness game for KZG in the algebraic group model.
The game samples α, runs the adversary on the SRS srs₁ α t, and the
adversary wins if:
- The commitment representation is valid for that SRS;
- The witness representation is valid for that SRS;
- The evaluation proof verifies:
verify_eval vk C z y w; - The claimed value is wrong:
y ≠ φ(z)where φ is the extracted polynomial.
An output whose representations do not match the supplied SRS loses.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reduction #
The reduction: converts a knowledge soundness adversary (in AGM) into a t-SDH adversary.
Given AGM adversary A that wins the knowledge soundness game:
- Run A on SRS to get (C_repr, z, y, w_repr)
- Extract φ from C_repr and ψ from w_repr
- Compute δ(X) = φ(X) - y - ψ(X) · (X - z)
- If δ = 0, A didn't actually break knowledge soundness
- If δ ≠ 0, then δ(α) = 0 (from the pairing check). Find a root r and guess r = α. If correct, compute t-SDH solution directly.
The reduction uses the same "guess the secret" strategy as poly_binding_to_tSDH:
when the guessed root r equals α, we know the secret and can construct the
t-SDH solution (c, g₁^(1/(α+c))).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pairing Helpers #
If e(g₁^a, g₂) = e(g₁^b, g₂^c) and e is non-degenerate, then a = b·c in the exponent.
This is the key property for extracting polynomial identities from pairing verification equations in the AGM.
Algebraic Helpers #
When both representations are valid for srs₁ α t, the verification
equation holds and y ≠ φ(z), the polynomial δ(X) = φ(X) - y - ψ(X) · (X - z)
is nonzero, has α as a root, and has degree at most t + 1.
Root Helpers (duplicated from PolyBinding since those are private) #
α ∈ roots(δ) implies α appears in roots.toList at some valid index.
roots.toList.length ≤ natDegree for nonzero polynomials.
When a root r of δ equals α, the tSDH check passes.
Knowledge Soundness Theorem #
KZG is knowledge-sound in the AGM: any AGM adversary that breaks knowledge soundness can be used to break t-SDH.
More precisely, the probability that an AGM adversary produces a valid
evaluation proof for an incorrect value is bounded by (t+1) × tSDH_Advantage.
The factor t+1 (vs t in polynomial binding) comes from δ having degree ≤ t+1
since δ(X) = φ(X) - y - ψ(X)·(X - z) involves the product ψ·(X - z).
Honest Algebraic Adversary #
The honest committer's output on basis pk: the commitment to φ with the
coefficients of φ as representation, the point z, the value φ(z), and
the witness commitment with the coefficients of witnessPoly φ z as
representation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The honest committer as an AGM adversary.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The honest commitment and witness elements are commit and create_witness.
Both honest representations pass the game's validity check for every basis.
The witness polynomial of a polynomial of degree at most t has degree at most t.
For φ of degree at most t, the honest representations extract to φ and
to witnessPoly φ z.
For φ of degree at most t, the honest output on srs₁ α t passes the
validity and pairing checks of KnowledgeSoundness_Game_Full and fails only
the mismatch condition y ≠ φ(z).