Skip to content

Formalizing the KZG polynomial commitment scheme in the Interactive Theorem Prover Isabelle.

Notifications You must be signed in to change notification settings

tobias-rothmann/KZG-Polynomial-Commitment-Scheme

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 

Repository files navigation

Formalizing the KZG-Polynomial-Commitment-Scheme in Isabelle/HOL

Isabelle/HOL

Isabelle/HOL is an open-source interactive theorem prover. The version used for this formalization is Isabelle2022 (as of writing this the most recent version).

Reference Paper

This formalization follows the original paper:
A. Kate, G. Zaverucha, and I. Goldberg. Polynomial commitments. Technical report, 2010. CACR 2010-10, Centre for Applied Cryptographic Research, University of Waterloo

First step is to prove the DL version.

Correctness

Correctness i.e. the interaction between an honest prover and an honest verifier, yields a correct result.

Proven.

Security Properties

The security properties are the same as in the paper. They are shown via game-based proofs, see the CryptHOL tutorial for details.

Polynomial Binding

(thanks to Katharina Kreuzer for providing the Elimination of repeated factors (ERF) algorithm, which allowed a complete factorization)

Proven.

Evaluation Binding

Proven.

Hiding

Proven.

Knowledge Soundness in the Algebraic Group Model (AGM)

Though this property is not explicitly stated in the original paper, it is commonly referred to and needed for zk-SNARK protocols, such as PLONK and Sonic.

Proven.

Batch version

Correctness

Proven.

Binding

Proven.

Hiding

Open.

Knowledge Soundness

Proven.

About

Formalizing the KZG polynomial commitment scheme in the Interactive Theorem Prover Isabelle.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published