Nominal State-Separating Proofs

Markus Krabbe Larsen; Carsten Schürmann

doi:10.1109/csf64896.2025.00038

Nominal State-Separating Proofs

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

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.

Original language	English
Title of host publication	2025 IEEE 38th Computer Security Foundations Symposium (CSF)
Number of pages	15
Publisher	IEEE
Publication date	16 Jun 2025
Pages	363-377
ISBN (Print)	9798331510817
ISBN (Electronic)	979-8-3315-1081-7, 979-8-3315-1082-4
DOIs	https://doi.org/10.1109/csf64896.2025.00038
Publication status	Published - 16 Jun 2025
Event	Computer Security Foundations Symposium - Santa Cruz, United States Duration: 16 Jun 2025 → 20 Jun 2025 Conference number: 38

Symposium

Symposium	Computer Security Foundations Symposium
Number	38
Country/Territory	United States
City	Santa Cruz
Period	16/06/2025 → 20/06/2025

Keywords

Formal verification
Modular cryptographic proofs
State-separating proofs
Coq
Nominal sets

Access to Document

10.1109/csf64896.2025.00038Licence: CC BY-SA

DIREC: Digital Research Centre Denmark
Godskesen, J. C. (PI), Barkhuus, L. (PI), Bonnet, P. (PI), Brabrand, C. (PI), Schürmann, C. (PI), Sekara, V. (PI), David, B. M. (PI), Husfeldt, T. (PI), Curticapean, R.-C. (PI), Limaye, N. (PI), Aumüller, M. (PI), Jacob, R. (PI), Risi, S. (PI), Wasowski, A. (PI), Okkels, C. B. (CoI), Berthelsen, K. H. (CoI), Larsen, M. K. (CoI), Schmidt, M. D. (CoI) & Ghaffari, M. (CoI)
Innovation Fund Denmark
01/10/2020 → 31/12/2025
Project: Research

Cite this

@inproceedings{7a377e33676b447590cb403c95160c3f,

title = "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.",

keywords = "Formal verification, Modular cryptographic proofs, State-separating proofs, Coq, Nominal sets",

author = "Larsen, \{Markus Krabbe\} and Carsten Sch{\"u}rmann",

year = "2025",

month = jun,

day = "16",

doi = "10.1109/csf64896.2025.00038",

language = "English",

isbn = "9798331510817",

pages = "363--377",

booktitle = "2025 IEEE 38th Computer Security Foundations Symposium (CSF)",

publisher = "IEEE",

address = "United States",

note = "Computer Security Foundations Symposium , CSF 2025 ; Conference date: 16-06-2025 Through 20-06-2025",

}

TY - GEN

T1 - Nominal State-Separating Proofs

AU - Larsen, Markus Krabbe

AU - Schürmann, Carsten

N1 - Conference code: 38

PY - 2025/6/16

Y1 - 2025/6/16

N2 - 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.

AB - 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.

KW - Formal verification

KW - Modular cryptographic proofs

KW - State-separating proofs

KW - Coq

KW - Nominal sets

UR - http://dx.doi.org/10.1109/csf64896.2025.00038

UR - https://eprint.iacr.org/2025/598

U2 - 10.1109/csf64896.2025.00038

DO - 10.1109/csf64896.2025.00038

M3 - Article in proceedings

SN - 9798331510817

SP - 363

EP - 377

BT - 2025 IEEE 38th Computer Security Foundations Symposium (CSF)

PB - IEEE

T2 - Computer Security Foundations Symposium

Y2 - 16 June 2025 through 20 June 2025

ER -

Nominal State-Separating Proofs

Abstract

Symposium

Keywords

Access to Document

Fingerprint

Projects

DIREC: Digital Research Centre Denmark

Cite this