Paper 2025/598
Nominal State-Separating Proofs
, IT University of Copenhagen, IT University of CopenhagenAbstract
State-separating proofs are a powerful tool to structure cryptographic arguments, so that they are amenable for mechanization, as has been shown through implementations, such as SSProve. However, the treatment of separation for heaps has never been satisfactorily addressed. In this work, we present the first comprehensive treatment of nominal state separation in state-separating proofs using nominal sets. We provide a Rocq library, called Nominal-SSProve, that builds on nominal state separation supporting mechanized proofs that appear more concise and arguably more elegant.
Note: Nominal-SSProve is available at: https://github.com/MarkusKL/nominal-ssprove
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- Published elsewhere. Computer Security Foundations Symposium (CSF)
- Keywords
- formal verificationmodular cryptographic proofsstate-separating proofsCoqnominal sets
- Contact author(s)
-
krml @ itu dk
carsten @ itu dk - History
- 2025-06-10: revised
- 2025-04-02: received
- See all versions
- Short URL
- https://ia.cr/2025/598
- License
-
CC BY-SA
BibTeX
@misc{cryptoeprint:2025/598,
author = {Markus Krabbe Larsen and Carsten Schürmann},
title = {Nominal State-Separating Proofs},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/598},
year = {2025},
url = {https://eprint.iacr.org/2025/598}
}
