Cryptology ePrint Archive: Report 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.

Category / Keywords: cryptographic protocols / computer-aided cryptography

Date: received 11 Mar 2021

Contact author: fdupress at gmail com,konrad kohbrok@aalto fi,oechsner@cs au dk

Available format(s): PDF | BibTeX Citation

Version: 20210311:190923 (All versions of this report)

Short URL: ia.cr/2021/326


[ Cryptology ePrint archive ]