Welcome to the resource topic for 2021/397
Title:
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
Authors: Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, 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 cryptographic 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. To illustrate the formal SSP methodology we prove security of ElGamal and PRF-based encryption. We also validate the SSProve approach by conducting two extended case studies. First, we formalize a security proof of the KEM-DEM public key encryption scheme. Second, we formalize security of the sigma-protocol zero-knowledge construction and the associated construction of commitment schemes. We then instantiate the proof and give concrete security bounds for Schnorr’s protocol.
ePrint: https://eprint.iacr.org/2021/397
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .