Paper 2026/1490
On the Formal Verification of Polynomial Commitments: two KZG constructions and the Algebraic Group Model
, Technical University of MunichAbstract
We formalize the notion of polynomial commitment schemes (PCSs) in the proof assistant Isabelle/HOL and formally verify the security proofs of two variants of the widely popular Kate, Zaverucha, and Goldberg (KZG) construction. Moreover, we formalize the Algebraic Group Model (AGM) by Fuchsbauer, Kiltz, and Loss using a novel constraint-programming-inspired approach. We formalize a reusable abstract definition of polynomial commitment schemes and define games for correctness, binding, hiding, and knowledge soundness/extractability. Based on this, we verify all applicable security proofs for two concrete PCS constructions: the standard (DL-)KZG and a batched KZG, using our AGM formalization in the knowledge-soundness proofs. Our proofs follow Shoup’s sequence-of-games approach, with machine-checked transitions, and are carried out in the CryptHOL framework for formal verification of cryptography in Isabelle. To our knowledge, this work is the first formalization of polynomial commitment schemes, the first formalization of the AGM, and the first formal verification of the security proofs for any concrete polynomial commitment scheme. This work lays the foundation for the formal verification of advanced cryptographic constructions, such as pairing-based zero-knowledge proofs (ZKPs) and succinct arguments.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Minor revision. ESORICS 2026
- Keywords
- Formal VerificationPolynomial CommitmentsAlgebraic Group ModelKZGIsabelle
- Contact author(s)
- tobias rothmann @ tum de
- History
- 2026-07-23: approved
- 2026-07-21: received
- See all versions
- Short URL
- https://ia.cr/2026/1490
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2026/1490,
author = {Tobias Rothmann},
title = {On the Formal Verification of Polynomial Commitments: two {KZG} constructions and the Algebraic Group Model},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/1490},
year = {2026},
url = {https://eprint.iacr.org/2026/1490}
}
