Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox

Francois Dupressoir, Konrad Kohbrok, Sabine Oechsner

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu


Machine-checked cryptography aims to reinforce confidence in the primitives and protocols that underpin all digital security. However, machine-checked proof techniques remain in practice difficult to apply to real-world constructions. A particular challenge is structured reasoning about complex constructions at different levels of abstraction. The State-Separating Proofs (SSP) methodology for guiding cryptographic proofs by Brzuska, Delignat-Lavaud, Fournet, Kohbrok and Kohlweiss (ASIACRYPT'18) is a promising contestant to support such reasoning. In this work, we explore how SSPs can guide EasyCrypt formalisations of proofs for modular constructions. Concretely, we propose a mapping from SSP to EasyCrypt concepts which enables us to enhance cryptographic proofs with SSP insights while maintaining compatibility with existing EasyCrypt proof support. To showcase our insights, we develop a formal security proof for the cryptobox family of public-key authenticated encryption schemes based on non-interactive key exchange and symmetric authenticated encryption. As a side effect, we obtain the first formal security proof for NaCl's instantiation of cryptobox. Finally we discuss changes to the practice of SSP on paper and potential implications for future tool designers.

OtsikkoProceedings - 2022 IEEE 35th Computer Security Foundations Symposium, CSF 2022
ISBN (elektroninen)978-1-6654-8417-6
DOI - pysyväislinkit
TilaJulkaistu - 2022
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaIEEE Computer Security Foundations Symposium - Haifa, Israel
Kesto: 7 elok. 202210 elok. 2022
Konferenssinumero: 35


NimiProceedings : IEEE Computer Security Foundations Symposium
ISSN (painettu)1940-1434


ConferenceIEEE Computer Security Foundations Symposium


Sukella tutkimusaiheisiin 'Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä