The sumcheck protocol, 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. However, none of these proof systems based on the sumcheck protocol enjoy a formally-verified security analysis. In this paper, we make progress in this direction by providing a formally verified security analysis of the sumcheck protocol using the interactive theorem prover Isabelle/HOL. We follow 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 facilitates 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 supports the development and formal verification of future cryptographic protocols using the sumcheck protocol as a building block.

翻译：和校验协议于1992年提出，是一种交互式证明，在计算复杂性理论和密码学的许多概率证明系统中发挥着关键作用，其中部分系统已得到部署。然而，这些基于和校验协议的证明系统均未进行过形式化验证的安全性分析。本文通过使用交互式定理证明器Isabelle/HOL对和校验协议提供形式化验证的安全性分析，在该方向上取得了进展。我们采用了一种通用且模块化的方法。首先，我们对公开抛币交互式证明进行了通用形式化。随后，定义了一个广义的和校验协议，并对其底层数学结构进行公理化，同时建立了其可靠性和完备性。最后，我们证明了这些公理对于多元多项式（和校验协议最初的设定）成立。我们的模块化分析使得基于不同数学结构的和校验实例能够轻松通过证明这些结构满足公理来完成形式化验证。此外，该分析还支持将和校验协议作为构建块来开发和形式化验证未来密码协议。