Cryptology ePrint Archive: Report 2021/397
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
Carmine Abate and Philipp G. Haselwarter and Exequiel Rivas and Antoine Van Muylder and Théo Winterhalter and Catalin Hritcu and Kenji Maillard and Bas Spitters
Abstract: State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way. While very 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 fully machine-checked crypto proofs in the Coq proof assistant. Moreover, SSProve is itself formalized in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles.
Category / Keywords: foundations / formal verification, modular cryptographic proofs, state-separating proofs, Coq
Date: received 24 Mar 2021
Contact author: catalin hritcu at gmail com
Available format(s): PDF | BibTeX Citation
Version: 20210327:071609 (All versions of this report)
Short URL: ia.cr/2021/397
[ Cryptology ePrint archive ]