Christian Badertscher, Ran Canetti, et al.
TCC 2020
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.
Christian Badertscher, Ran Canetti, et al.
TCC 2020
Ehud Aharoni, Nir Drucker, et al.
CSCML 2023
Jonathan Bootle, Vadim Lyubashevsky, et al.
ESORICS 2021
Arnab Bag, Debadrita Talapatra, et al.
PETS 2023