You are looking at a specific version 20210823:063640 of this paper. See the latest version.

Paper 2021/1078

Reflection, Rewinding, and Coin-Toss in EasyCrypt

Denis Firsov and Dominique Unruh

Abstract

In this paper we derive a suit 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 reflection and rewindability results to prove the security of a coin-toss protocol.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Preprint. MINOR revision.
Keywords
cryptographyformal methodsEasyCryptreflectionrewindabilitycommitmentsbindingcoin-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
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.