Formal Verification of the Sumcheck Protocol

这篇论文介绍了1992年提出的Sumcheck协议，它是计算复杂性理论和密码学中许多概率证明系统的关键组成部分，其中一些已经得到了应用。然而，基于Sumcheck协议的这些证明系统中没有一个享有正式验证的安全分析。本文通过使用交互式定理证明器Isabelle/HOL，为Sumcheck协议提供了正式验证的安全分析。我们采用了一种通用且模块化的方法。首先，我们对公共币交互式证明进行了一般形式化。然后，我们定义了一个广义的Sumcheck协议，对其基础数学结构进行了公理化，并证明了其完备性和正确性。最后，我们证明了这些公理适用于多元多项式，这是Sumcheck协议的原始设置。我们的模块化分析使得对基于不同数学结构的Sumcheck实例进行正式验证变得容易，只需证明这些结构满足公理即可。此外，该分析支持使用Sumcheck协议作为构建块开发和正式验证未来的密码协议。

提供正式验证的sumcheck协议安全性分析，以及为将来使用sumcheck协议作为构建块的加密协议开发和正式验证提供支持。

使用交互式定理证明器Isabelle/HOL提供了sumcheck协议的正式验证安全分析。通过一般和模块化的方法，定义了公共硬币交互证明的形式化，然后定义了广义的sumcheck协议，证明了其正确性和完整性，并证明了这些公理适用于多元多项式，这是sumcheck协议的原始设置。

论文的亮点在于提供了sumcheck协议的正式验证安全分析，支持了将来使用sumcheck协议作为构建块的加密协议开发和正式验证。该分析还支持使用不同的数学结构基于sumcheck协议的不同实例的形式化验证，实现了模块化。论文还提供了开源代码和实验数据集。

最近的相关研究包括：基于交互式证明的加密协议，交互式证明在计算复杂性理论和密码学中的应用等。