Reflection, Rewinding, and Coin-Toss in EasyCrypt
summary
Derives a concrete library of lemmas that reflect EasyCrypt procedures into explicit distributions d_a over final module states and shows composition via monadic bind so semantics of a;b equals bind(d_a,d_b). Builds generic support for probabilistic reflection to prove Jensen, averaging, and finite probabilistic approximation inside EasyCrypt. Formalizes rewindable modules with injective state encoding plus getstate/setstate and proves commutativity and multiplication properties. Uses these tools to mechanize a coin toss proof that cheating Alice wins only with negligible probability given binding commitments.
AI-written summary · about
chapters (8)
- 0:00Start
- 1:19Review Notation
- 4:03Step 3
- 8:18Finite Probabilistic Approximation
- 8:35The Averaging Technique
- 9:16Rewind Ability of Program Modules
- 13:32Mental Experiment
- 14:26Attack against the Binding of a Commitment Scheme
related talks
26mA Core Calculus for Equational Proofs of Cryptographic Protocols
01h 09mCrypto + ML 1
57mThe Cryptographic Lens: Visions of our Past and Future
20mOn the computational hardness needed for quantum cryptography
48mCommitments to Quantum States
52mHash-based Folding Schemes
01h 01mCircularity Based IO, Part 1
49mQuantum Cryptanalysis