[Resource Topic] 2017/753: CryptHOL: Game-based Proofs in Higher-order Logic

Welcome to the resource topic for 2017/753

CryptHOL: Game-based Proofs in Higher-order Logic

Authors: David A. Basin, Andreas Lochbihler, S. Reza Sefidgar


Game-based proofs are a well-established paradigm for structuring security arguments and simplifying their understanding. We present a novel framework, CryptHOL, for rigorous game-based proofs that is supported by mechanical theorem proving. CryptHOL is based on a new semantic domain with an associated functional programming language for expressing games. We embed our framework in the Isabelle/HOL theorem prover and, using the theory of relational parametricity, we tailor Isabelle’s existing proof automation to game-based proofs. By basing our framework on a conservative extension of higher-order logic and providing automation support, the resulting proofs are trustworthy and comprehensible, and the framework is extensible and widely applicable. We evaluate our framework by formalizing different game-based proofs from the literature and comparing the results with existing formal-methods tools.

ePrint: https://eprint.iacr.org/2017/753

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .