Reflection, Rewinding, and Coin-Toss in EasyCrypt

Denis Firsov; Dominique Unruh

Paper 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.

Note: has some additional explicit proofs

Metadata

Available format(s): PDF
Category: Foundations
Publication info: Published elsewhere. Minor revision. CPP 2022
DOI: 10.1145/3497775.3503693
Keywords: cryptography formal methods EasyCrypt reflection rewindability commitments binding coin-toss
Contact author(s): denis firsov @ gmail com
History: 2022-01-17: revised; 2021-08-23: received; See all versions
Short URL: https://ia.cr/2021/1078
License: CC BY

BibTeX

@misc{cryptoeprint:2021/1078,
      author = {Denis Firsov and Dominique Unruh},
      title = {Reflection, Rewinding, and Coin-Toss in {EasyCrypt}},
      howpublished = {Cryptology {ePrint} Archive, Paper 2021/1078},
      year = {2021},
      doi = {10.1145/3497775.3503693},
      url = {https://eprint.iacr.org/2021/1078}
}