TY - GEN
T1 - SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
AU - Abate, Carmine
AU - Haselwarter, Philipp G.
AU - Rivas, Exequiel
AU - Van Muylder, Antoine Joaquim S
AU - Winterhalter, Théo
AU - Hrițcu, Cătălin
AU - Maillard, Kenji
AU - Spitters, Bas
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85124033279&partnerID=8YFLogxK
U2 - 10.1109/CSF51468.2021.00048
DO - 10.1109/CSF51468.2021.00048
M3 - Conference paper
VL - 1
T3 - 2021 IEEE 34TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2021)
SP - 608
EP - 622
BT - 2021 IEEE 34th Computer Security Foundations Symposium (CSF)
PB - IEEE Computer Society
T2 - 2021 IEEE 34th Computer Security Foundations Symposium (CSF)
Y2 - 21 June 2021
ER -