Mechanizing the Proof of Adaptive, Information-Theoretic Security of Cryptographic Protocols in the Random Oracle Model
2017 IEEE 30th Computer Security Foundations Symposium (CSF) (2017)
Santa Barbara, California, USA
Aug. 21, 2017 to Aug. 25, 2017
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSF.2017.36
We 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.
Protocols, Games, Databases, Servers, Cryptography, Upper bound
A. Stoughton and M. Varia, "Mechanizing the Proof of Adaptive, Information-Theoretic Security of Cryptographic Protocols in the Random Oracle Model," 2017 IEEE 30th Computer Security Foundations Symposium (CSF), Santa Barbara, California, USA, 2017, pp. 83-99.