Nominal State-Separating Proofs

Markus Krabbe Larsen; Carsten Schürmann

doi:10.1109/csf64896.2025.00038

Nominal State-Separating Proofs

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	2025 IEEE 38th Computer Security Foundations Symposium (CSF)
Antal sider	15
Forlag	IEEE
Publikationsdato	16 jun. 2025
Sider	363-377
ISBN (Trykt)	9798331510817
ISBN (Elektronisk)	979-8-3315-1081-7, 979-8-3315-1082-4
DOI	https://doi.org/10.1109/csf64896.2025.00038
Status	Udgivet - 16 jun. 2025
Begivenhed	Computer Security Foundations Symposium - Santa Cruz, USA Varighed: 16 jun. 2025 → 20 jun. 2025 Konferencens nummer: 38

Symposium

Symposium	Computer Security Foundations Symposium
Nummer	38
Land/Område	USA
By	Santa Cruz
Periode	16/06/2025 → 20/06/2025

Adgang til dokumentet

10.1109/csf64896.2025.00038Licens: 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 (IFD)
01/10/2020 → 30/09/2025
Projekter: Projekt › Forskning

Citationsformater

@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

Adgang til dokumentet

Fingeraftryk

Projekter

DIREC: Digital Research Centre Denmark

Citationsformater