Cryptology ePrint Archive: Report 2017/753

CryptHOL: Game-based Proofs in Higher-order Logic

David A. Basin and Andreas Lochbihler and S. Reza Sefidgar

Abstract: 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.

Category / Keywords: foundations / Provable Security, Game-based Proofs, Theorem Proving, Higher-order Logic, Isabelle/HOL

Original Publication (in the same form): IACR-JOC-2020

Date: received 3 Aug 2017, last revised 16 May 2020

Contact author: mail at andreas-lochbihler de

Available format(s): PDF | BibTeX Citation

Note: This is the revised version that has been accepted at the Journal of Cryptology.

Version: 20200516:174011 (All versions of this report)

Short URL: ia.cr/2017/753