Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Formalisation of the KZG Polynomial Commitment Schemes in EasyCrypt

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Palak,
  • Thomas Haines

摘要

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.