Nominal State-Separating Proofs

Markus Krabbe Larsen; Carsten Schürmann

Paper 2025/598

Nominal State-Separating Proofs

Markus Krabbe Larsen, IT University of Copenhagen

Carsten Schürmann, IT University of Copenhagen

Abstract

State-separting 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 Coq library, called Nominal-SSProve, that builds on nominal state separation supporting mechanized proofs that appear more concise and arguably more elegant.

Note: Supplementary material available at: https://github.com/MarkusKL/nominal-ssprove

Metadata

Available format(s): PDF
Category: Foundations
Publication info: Preprint.
Keywords: formal verification modular cryptographic proofs state-separating proofs Coq nominal sets
Contact author(s): krml @ itu dk
carsten @ itu dk
History: 2025-04-04: approved; 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}
}