POPL 2022 (series) / CPP 2022 (series) / CPP 2022 / Reflection, Rewinding, and Coin-Toss in EasyCrypt
Reflection, Rewinding, and Coin-Toss in EasyCryptRemote
Mon 17 Jan 2022 15:30 - 15:55 at Salon III - Security and Distributed Systems Chair(s): Alwyn Goodloe
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.
Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change
Mon 17 Jan
Displayed time zone: Eastern Time (US & Canada) change
15:30 - 17:10 | Security and Distributed SystemsCPP at Salon III Chair(s): Alwyn Goodloe NASA Langley Research Center | ||
15:30 25mTalk | Reflection, Rewinding, and Coin-Toss in EasyCryptRemote CPP Pre-print Media Attached | ||
15:55 25mTalk | A verified algebraic representation of Cairo program executionRemote CPP Jeremy Avigad Carnegie Mellon University, USA, Lior Goldberg Starkware Industries Ltd., David Levit Starkware Industries Ltd., Yoav Seginer cdl-lang.org, Netherlands, Alon Titelman Starkware Industries Ltd. Pre-print | ||
16:20 25mTalk | Formal Verification of a Distributed Dynamic Reconfiguration ProtocolInPerson CPP William Schultz Northeastern University, Ian Dardik Northeastern University, Stavros Tripakis Northeastern University Pre-print | ||
16:45 25mTalk | Forward build systems, formallyInPerson CPP Link to publication | ||