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