Stoughton, AlleyVaria, Mayank2021-10-272021-10-272017-08-21A. Stoughton, M. Varia. 2017. "Mechanizing the Proof of Adaptive, Information-Theoretic Security of Cryptographic Protocols in the Random Oracle Model." https://ieeexplore.ieee.org/document/8049653/. 30th IEEE Computer Security Foundations Symposium. Santa Barbara, CA, 2017-08-21 - 2017-08-25. https://doi.org/10.1109/CSF.2017.36https://hdl.handle.net/2144/43227We report on our research on proving the security of multi-party cryptographic protocols using the EASYCRYPT proof assistant. We work in the computational model using the sequence of games approach, and define honest-butcurious (semi-honest) security using a variation of the real/ideal paradigm in which, for each protocol party, an adversary chooses protocol inputs in an attempt to distinguish the party's real and ideal games. Our proofs are information-theoretic, instead of being based on complexity theory and computational assumptions. We employ oracles (e.g., random oracles for hashing) whose encapsulated states depend on dynamically-made, nonprogrammable random choices. By limiting an adversary's oracle use, one may obtain concrete upper bounds on the distances between a party's real and ideal games that are expressed in terms of game parameters. Furthermore, our proofs work for adaptive adversaries, ones that, when choosing the value of a protocol input, may condition this choice on their current protocol view and oracle knowledge. We provide an analysis in EASYCRYPT of a three party private count retrieval protocol. We emphasize the lessons learned from completing this proof.en-USConference materials10.1109/CSF.2017.36362753