**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

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''.

### License

### Topics

- Computer science/Security
- Computer science/Algorithms/Distributed
- Computer science/Algorithms/Randomized

### Related publications

- Formal Verification of the Sumcheck Protocol, CSF 2024

### Session Sumcheck_Protocol

- Probability_Tools
- Public_Coin_Proofs
- Substitutions
- Abstract_Multivariate_Polynomials
- Sumcheck_Protocol
- Completeness_Proof
- Soundness_Proof
- Sumcheck_as_Public_Coin_Proof
- Polynomial_Instantiation
- Univariate_Roots_Bound
- Roots_Bounds
- Concrete_Multivariate_Polynomials