SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Joaquim S Van Muylder, Théo Winterhalter, Cătălin Hrițcu, Kenji Maillard, Bas Spitters

Onderzoeksoutput: Conference paper

Samenvatting

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.
Originele taal-2English
Titel2021 IEEE 34th Computer Security Foundations Symposium (CSF)
UitgeverijIEEE Computer Society
Pagina's608-622
Volume1
DOI's
StatusPublished - 2021
Evenement2021 IEEE 34th Computer Security Foundations Symposium (CSF) -
Duur: 21 jun 2021 → …

Publicatie series

Naam2021 IEEE 34TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2021)
ISSN van geprinte versie1940-1434

Conference

Conference2021 IEEE 34th Computer Security Foundations Symposium (CSF)
Verkorte titelCSF 2021
Periode21/06/21 → …

Vingerafdruk

Duik in de onderzoeksthema's van 'SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq'. Samen vormen ze een unieke vingerafdruk.

Citeer dit