Email Gateway (Feb 07 2024 at 08:12): Email Gateway (Feb 07 2024 at 08:12):From: Dmitriy Traytel <traytel@di.ku.dk>
Interactive proofs about (the other kind of) interactive proofs<https://en.wikipedia.org/wiki/Interactive_proof_system>? This precisely what Azucena Garvia, Christoph Sprenger, and Jonathan Bootle have been doing recently:
The Sumcheck Protocol
The sumcheck protocol, first introduced in 1992, is an interactive proof which is a key component of many probabilistic proof systems in computational complexity theory and cryptography, some of which have been deployed. We provide a formally verified security analysis of the sumcheck protocol, following a general and modular approach. First, we give a general formalization of public-coin interactive proofs. We then define a generalized sumcheck protocol for which we axiomatize the underlying mathematical structure and we establish its soundness and completeness. Finally, we prove that these axioms hold for multivariate polynomials, the original setting of the sumcheck protocol. Our modular analysis will facilitate formal verification of sumcheck instances based on different mathematical structures with little effort, by simply proving that these structures satisfy the axioms. Moreover, the analysis will encourage the development and formal verification of future probabilistic proof systems using the sumcheck protocol as a building block. The paper presenting this formalization is to appear at CSF 2024 under the title Formal Verification of the Sumcheck Protocol.
https://www.isa-afp.org/entries/Sumcheck_Protocol.html
Enjoy!
Last updated: Apr 29 2024 at 04:18 UTC