SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Philipp G. Haselwarter; Exequiel Rivas; Antoine Van Muylder; Théo Winterhalter; Carmine Abate; Nikolaj Sidorenco; Cǎtǎlin Hriţcu; Kenji Maillard; Bas Spitters

doi:10.1145/3594735

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Cǎtǎlin Hriţcu, Kenji Maillard, Bas Spitters

Institut for Datalogi

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avis › Tidsskriftartikel › Forskning › peer review

4 Citationer (Scopus)

Abstract

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While 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 machine-checked cryptographic proofs in the Coq proof assistant. Moreover, SSProve is itself fully 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 SSProve, we use it to mechanize the simple security proofs of ElGamal and pseudo-random-function-based encryption. We also validate the SSProve approach by conducting two more substantial case studies: First, we mechanize an SSP security proof of the key encapsulation mechanism-data encryption mechanism (KEM-DEM) public key encryption scheme, which led to the discovery of an error in the original paper proof that has since been fixed. Second, we use SSProve to formally prove security of the sigma-protocol zero-knowledge construction, and we moreover construct a commitment scheme from a sigma-protocol to compare with a similar development in CryptHOL. We instantiate the security proof for sigma-protocols to give concrete security bounds for Schnorr's sigma-protocol.

Originalsprog	Engelsk
Artikelnummer	15
Tidsskrift	ACM Transactions on Programming Languages and Systems
Vol/bind	45
Nummer	3
Sider (fra-til)	61
ISSN	0164-0925
DOI	https://doi.org/10.1145/3594735
Status	Udgivet - jul. 2023

Adgang til dokumentet

10.1145/3594735Licens: CC BY

Andre filer og links

Link to publication in Scopus

Citationsformater

@article{1e610b433ec34bc1a847f069e0756a3e,

title = "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq",

abstract = "State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While 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 machine-checked cryptographic proofs in the Coq proof assistant. Moreover, SSProve is itself fully 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 SSProve, we use it to mechanize the simple security proofs of ElGamal and pseudo-random-function-based encryption. We also validate the SSProve approach by conducting two more substantial case studies: First, we mechanize an SSP security proof of the key encapsulation mechanism-data encryption mechanism (KEM-DEM) public key encryption scheme, which led to the discovery of an error in the original paper proof that has since been fixed. Second, we use SSProve to formally prove security of the sigma-protocol zero-knowledge construction, and we moreover construct a commitment scheme from a sigma-protocol to compare with a similar development in CryptHOL. We instantiate the security proof for sigma-protocols to give concrete security bounds for Schnorr's sigma-protocol.",

keywords = "formal verification, game-based proofs, High-assurance cryptography, machine-checked proofs, modular proofs, probabilistic relational program logic, state-separating proofs",

author = "Haselwarter, {Philipp G.} and Exequiel Rivas and {Van Muylder}, Antoine and Th{\'e}o Winterhalter and Carmine Abate and Nikolaj Sidorenco and Cǎtǎlin Hri{\c t}cu and Kenji Maillard and Bas Spitters",

note = "Publisher Copyright: {\textcopyright} 2023 Copyright held by the owner/author(s).",

year = "2023",

month = jul,

doi = "10.1145/3594735",

language = "English",

volume = "45",

pages = "61",

journal = "ACM Transactions on Programming Languages and Systems",

issn = "0164-0925",

publisher = "Association for Computing Machinery",

number = "3",

}

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. / Haselwarter, Philipp G.; Rivas, Exequiel; Van Muylder, Antoine et al.
I: ACM Transactions on Programming Languages and Systems, Bind 45, Nr. 3, 15, 07.2023, s. 61.

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avis › Tidsskriftartikel › Forskning › peer review

TY - JOUR

T1 - SSProve

T2 - A Foundational Framework for Modular Cryptographic Proofs in Coq

AU - Haselwarter, Philipp G.

AU - Rivas, Exequiel

AU - Van Muylder, Antoine

AU - Winterhalter, Théo

AU - Abate, Carmine

AU - Sidorenco, Nikolaj

AU - Hriţcu, Cǎtǎlin

AU - Maillard, Kenji

AU - Spitters, Bas

PY - 2023/7

Y1 - 2023/7

N2 - State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While 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 machine-checked cryptographic proofs in the Coq proof assistant. Moreover, SSProve is itself fully 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 SSProve, we use it to mechanize the simple security proofs of ElGamal and pseudo-random-function-based encryption. We also validate the SSProve approach by conducting two more substantial case studies: First, we mechanize an SSP security proof of the key encapsulation mechanism-data encryption mechanism (KEM-DEM) public key encryption scheme, which led to the discovery of an error in the original paper proof that has since been fixed. Second, we use SSProve to formally prove security of the sigma-protocol zero-knowledge construction, and we moreover construct a commitment scheme from a sigma-protocol to compare with a similar development in CryptHOL. We instantiate the security proof for sigma-protocols to give concrete security bounds for Schnorr's sigma-protocol.

AB - State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While 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 machine-checked cryptographic proofs in the Coq proof assistant. Moreover, SSProve is itself fully 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 SSProve, we use it to mechanize the simple security proofs of ElGamal and pseudo-random-function-based encryption. We also validate the SSProve approach by conducting two more substantial case studies: First, we mechanize an SSP security proof of the key encapsulation mechanism-data encryption mechanism (KEM-DEM) public key encryption scheme, which led to the discovery of an error in the original paper proof that has since been fixed. Second, we use SSProve to formally prove security of the sigma-protocol zero-knowledge construction, and we moreover construct a commitment scheme from a sigma-protocol to compare with a similar development in CryptHOL. We instantiate the security proof for sigma-protocols to give concrete security bounds for Schnorr's sigma-protocol.

KW - formal verification

KW - game-based proofs

KW - High-assurance cryptography

KW - machine-checked proofs

KW - modular proofs

KW - probabilistic relational program logic

KW - state-separating proofs

UR - http://www.scopus.com/inward/record.url?scp=85173587757&partnerID=8YFLogxK

U2 - 10.1145/3594735

DO - 10.1145/3594735

M3 - Journal article

AN - SCOPUS:85173587757

SN - 0164-0925

VL - 45

SP - 61

JO - ACM Transactions on Programming Languages and Systems

JF - ACM Transactions on Programming Languages and Systems

IS - 3

M1 - 15

ER -

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Abstract

Adgang til dokumentet

Andre filer og links

Fingeraftryk

Citationsformater