Formalisation of the KZG polynomial commitment schemes in EasyCrypt

Palak; Thomas Haines

Paper 2025/1972

Formalisation of the KZG polynomial commitment schemes in EasyCrypt

Palak

, Australian National University

Thomas Haines

, Australian National University

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.

Note: Fixed typo in section heading 4.1

Metadata

Available format(s): PDF
Category: Public-key cryptography
Publication info: Published elsewhere. Minor revision. ESORICS 2025
Keywords: Formal Verification EasyCrypt Polynomial Commitment Schemes
Contact author(s): palak palak @ anu edu au
thomas haines @ anu edu au
History: 2025-10-29: revised; 2025-10-21: received; See all versions
Short URL: https://ia.cr/2025/1972
License: CC BY

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}
}