About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
CSF 2024
Conference paper
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.