SSProve : a foundational framework for modular cryptographic proofs in Coq

author
Haselwarter, Philipp G.
Van Muylder, Antoine
Winterhalter, Théo
Abate, Carmine
Sidorenco, Nikolaj
Hriţcu, Cǎtǎlin
Maillard, Kenji
Spitters, Bas
statement of authorship
Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Cǎtǎlin Hriţcu, Kenji Maillard, Bas Spitters
source
ACM Transactions on Programming Languages and Systems
publisher
ACM
journal volume number month
vol. 45, 3
year of publication
pages
art. 15
ISSN
0164-0925
notes
Bibliogr.: 98 ref
Open Access
Open Access
scientific publication
teaduspublikatsioon
language
inglise
keyword
game-based proofs
high-assurance cryptography
machine-checked proofs
probabilistic relational program logic
state-separating proofs
category (general)
Haselwarter, P., Rivas, E., Van Muylder, A., Winterhalter, T., Abate, C., Sidorenco, N., Hriţcu, C., Maillard, K., Spitters, B. SSProve : a foundational framework for modular cryptographic proofs in Coq // ACM Transactions on Programming Languages and Systems (2023) vol. 45, 3, art. 15. https://doi.org/10.1145/3594735