Paper 2021/326

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

François Dupressoir, University of Bristol
Konrad Kohbrok, Aalto University
Sabine Oechsner, University of Edinburgh
Abstract

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.

Note: This revision fixes a few typos, addresses some issues with the pen-and-paper proof sketch, and refines a reference for clarity.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Minor revision. CSF 2022
DOI
10.1109/CSF54842.2022.9919671
Keywords
computer-aided cryptography
Contact author(s)
fdupress @ gmail com
konrad kohbrok @ datashrine de
s oechsner @ ed ac uk
History
2023-11-08: last of 4 revisions
2021-03-11: received
See all versions
Short URL
https://ia.cr/2021/326
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2021/326,
      author = {François Dupressoir and Konrad Kohbrok and Sabine Oechsner},
      title = {Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox},
      howpublished = {Cryptology ePrint Archive, Paper 2021/326},
      year = {2021},
      doi = {10.1109/CSF54842.2022.9919671},
      note = {\url{https://eprint.iacr.org/2021/326}},
      url = {https://eprint.iacr.org/2021/326}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.