一句话：提出首个在 Coq 中机器检验状态分离密码证明的通用框架 SSProve，结合模块化证明与概率关系程序逻辑。
状态分离证明（SSP）是一种用代数定律模块化组织基于游戏密码证明的方法，但此前缺乏完整形式化与工具支持。本文提出 SSProve，首个支持机器检验状态分离证明的通用验证框架。它将 SSP 高层模块化证明与概率关系程序逻辑结合，并在 Coq 中完整形式化，包括 SSP 代数定律、程序逻辑可靠性及两种风格的联系。作者机械化 ElGamal 和 PRF 加密证明，完成 KEM-DEM 公钥加密的 SSP 证明并发现原论文错误；还形式化 sigma 协议零知识与承诺方案，与 CryptHOL 比较，并给出 Schnorr 协议的具体安全界。
State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalizing the lower-level details, which together enable constructing machine-checked cryptographic proofs in the Coq proof assistant. Moreover, SSProve is itself fully formalized in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles. To illustrate SSProve, we use it to mechanize the simple security proofs of ElGamal and pseudo-random-function–based encryption. We also validate the SSProve approach by conducting two more substantial case studies: First, we mechanize an SSP security proof of the key encapsulation mechanism–data encryption mechanism (KEM-DEM) public key encryption scheme, which led to the discovery of an error in the original paper proof that has since been fixed. Second, we use SSProve to formally prove security of the sigma-protocol zero-knowledge construction, and we moreover construct a commitment scheme from a sigma-protocol to compare with a similar development in CryptHOL. We instantiate the security proof for sigma-protocols to give concrete security bounds for Schnorr’s sigma-protocol.
@article{paperbot2127,
title = {SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq},
author = {Philipp G. Haselwarter and Exequiel Rivas and Antoine Van Muylder and Théo Winterhalter and Carmine Abate and Nikolaj Sidorenco and Cătălin Hriţcu and Kenji Maillard and Bas Spitters},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {3},
year = {2023},
doi = {10.1145/3594735}
}