You are looking at a specific version 20210526:113037 of this paper. See the latest version.

Paper 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.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. CSF 2021 (34th IEEE Computer Security Foundations Symposium)
Keywords
formal verificationmodular cryptographic proofsstate-separating proofsCoq
Contact author(s)
catalin hritcu @ gmail com
History
2023-11-08: last of 7 revisions
2021-03-27: received
See all versions
Short URL
https://ia.cr/2021/397
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.