Paper 2021/1078 Original: eprint.iacr.org/2021/1078 ↗
Reflection, Rewinding, and Coin-Toss in EasyCrypt
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.
Metadata
- Available format(s)
PDF- Category
- Foundations
- Publication info
- Preprint.
- History
- 2022-01-17: last updated
- 2021-08-23: published
- Short URL
- https://ia.cr/2021/1078
- License
- https://creativecommons.org/licenses/by/4.0/
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},
url = {https://eprint.iacr.org/2021/1078}
}