Paper 2025/1972 Original: eprint.iacr.org/2025/1972 ↗
Formalisation of the KZG polynomial commitment schemes in EasyCrypt
Abstract
In this paper, we present formally verified proofs of the popular KZG Polynomial Commitment Schemes (PCSs), including the security proofs for the properties of correctness, polynomial binding, evaluation binding and hiding. Polynomial commitment schemes have various applications in cryptography and computer science, including verifiable computation, blockchain and cryptocurrencies, secure multi-party computation as well as in the construction of ZK-SNARKs. To validate security, we utilise EasyCrypt, an interactive theorem prover that allows for formal verification of cryptographic primitives and protocols. This approach enforces correct proofs which cover all required cases and formalising assumptions reducing the risk of overlooked vulnerabilities. This formalisation validates the current understanding of KZG's PCSs as secure while clarifying various issues in the original claims.
Metadata
- Available format(s)
PDF- Category
- Public-key cryptography
- Publication info
- Preprint.
- History
- 2025-10-29: last updated
- 2025-10-21: published
- Short URL
- https://ia.cr/2025/1972
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2025/1972,
author = {Palak and Thomas Haines},
title = {Formalisation of the KZG polynomial commitment schemes in EasyCrypt},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/1972},
year = {2025},
url = {https://eprint.iacr.org/2025/1972}
}