Formal Verification of the Sumcheck Protocol

Abstract

The sumcheck protocol, first introduced in 1992, is an interactive proof which is a key component of many proof systems in computational complexity theory and cryptography, some of which have been deployed. However, none of these proof systems enjoy a formally-verified security analysis. In this paper, we make progress in this direction by providing a formal verified security analysis of the sumcheck protocol using the Isabelle automated theorem prover. We follow a modular approach. First, we establish the protocol’s completeness and soundness for an abstract version of the protocol where the required underlying mathematical structure is axiomatized. Second, we prove that these axioms hold for multivariate polynomials, the original setting of the sumcheck protocol. Our modular analysis will facilitate formal verification for sumcheck variants based on different mathematical structures (e.g., tensor codes) with little effort, by simply proving that these structures satisfy the axioms. Moreover, the analysis will encourage the development and formal verification of future cryptographic protocols using the sumcheck protocol as a building block.