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 sufficient 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 (with major differences): ESOP 2016, LNCS 9632, pp. 503–531
DOI: 10.1007/978-3-662-49498-1_20

Date: received 3 Aug 2017

Contact author: andreas lochbihler at inf ethz ch

Available format(s): PDF | BibTeX Citation

Version: 20170807:163633 (All versions of this report)

Short URL: ia.cr/2017/753

Discussion forum: Show discussion | Start new discussion