Paper 2021/326
Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
François Dupressoir and Konrad Kohbrok and Sabine Oechsner
Abstract
The State-Separating Proofs (SSP) framework by Brzuska et al. (ASIACRYPT’18) proposes a novel way to perform modular, code-based game-playing proofs. In this work, we demonstrate the potential of SSP for guiding the development of formally verified security proofs of composed real-world protocols in the EasyCrypt proof assistant. In particular, we show how to extract an EasyCrypt formalization skeleton from an SSP formalization. As a concrete example, we study the Cryptobox protocol, a KEM-DEM construction that combines DH key agreement with authenticated encryption. We develop a Cryptobox formalization using SSP both on paper and in EasyCrypt, exploring the usefulness of the SSP method in conjunction with an automated proof construction and verification tool.
Metadata
- Available format(s)
- Category
- Cryptographic protocols
- Publication info
- Preprint. MINOR revision.
- Keywords
- computer-aided cryptography
- Contact author(s)
- fdupress @ gmail com,konrad kohbrok @ aalto fi,oechsner @ cs au dk
- History
- 2023-11-08: last of 4 revisions
- 2021-03-11: received
- See all versions
- Short URL
- https://ia.cr/2021/326
- License
-
CC BY