Cryptology ePrint Archive: Report 2021/1078

Reflection, Rewinding, and Coin-Toss in EasyCrypt

Denis Firsov and Dominique Unruh

Abstract: In this paper we derive a suite of lemmas which allows users to internally reflect EasyCrypt programs into distributions which correspond to their denotational semantics (probabilistic reflection). Based on this we develop techniques for reasoning about rewinding of adversaries in EasyCrypt. (A widely used technique in cryptology.) We use our reflection and rewindability results to prove the security of a coin-toss protocol.

Category / Keywords: foundations / cryptography, formal methods, EasyCrypt, reflection, rewindability, commitments, binding, coin-toss

Original Publication (with minor differences): CPP 2022

Date: received 22 Aug 2021, last revised 17 Jan 2022

Contact author: denis firsov at gmail com

Available format(s): PDF | BibTeX Citation

Note: has some additional explicit proofs

Version: 20220117:162400 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]