You are looking at a specific version 20210311:190923 of this paper. See the latest version.

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)
PDF
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
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.