Email Gateway (Jul 13 2026 at 12:36): Email Gateway (Jul 13 2026 at 12:36):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Polynomial Commitment Schemes by Tobias Rothmann
Dear all,
I’m happy to announce a new AFP entry.
Polynomial Commitment Schemes
by Tobias Rothmann
This entry formalizes polynomial commitment schemes (PCSs) and the security
proofs of two variants of the Kate–Zaverucha–Goldberg (KZG) construction. We
define an abstract PCS interface and games for correctness, polynomial binding,
evaluation binding, hiding, and knowledge soundness. We also formalize symmetric
pairings, the DL, t-DL, t-SDH, and t-BSDH assumptions, and the Algebraic Group
Model (AGM) of Fuchsbauer, Kiltz, and Loss using a constraint-programming-inspired
approach. Based on these definitions, we verify correctness, polynomial binding,
evaluation binding, and knowledge soundness for the standard and batched KZG
constructions, as well as weak evaluation hiding for the standard KZG. The
security proofs are carried out in the CryptHOL framework and follow Shoup's
sequence-of-games approach with machine-checked game transitions.
https://isa-afp.org/entries/Polynomial_Commitment_Schemes.html
Enjoy,
René
Last updated: Jul 22 2026 at 14:00 UTC