Paper 2025/598 Original: eprint.iacr.org/2025/598 ↗
Nominal State-Separating Proofs
Abstract
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.
Metadata
- Available format(s)
PDF- Category
- Foundations
- Publication info
- Preprint.
- History
- 2025-06-10: last updated
- 2025-04-02: published
- Short URL
- https://ia.cr/2025/598
- License
- https://creativecommons.org/licenses/by-sa/4.0/
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}
}