Aarhus University Seal

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Carmine Abate, MPI-SP
  • ,
  • Philipp G. Haselwarter
  • Exequiel Rivas, Inria
  • ,
  • Antoine Van Muylder, Vrije Universiteit Brussel
  • ,
  • Théo Winterhalter, MPI-SP
  • ,
  • Cătălin Hriţcu, MPI-SP
  • ,
  • Kenji Maillard, Inria
  • ,
  • Bas Spitters

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.

Original languageEnglish
Title of host publication2021 IEEE 34th Computer Security Foundations Symposium (CSF)
Number of pages15
Publication year2021
ISBN (Electronic)978-1-7281-7607-9
Publication statusPublished - 2021
Event34th IEEE Computer Security Foundations Symposium - Virtual, Online, United States
Duration: 21 Jun 202125 Jun 2021
Conference number: 34


Conference34th IEEE Computer Security Foundations Symposium
LandUnited States

See relations at Aarhus University Citationformats

ID: 227594746