Cryptology ePrint Archive: Report 2018/941

A tutorial introduction to CryptHOL

Andreas Lochbihler and S. Reza Sefidgar

Abstract: This tutorial demonstrates how cryptographic security notions, constructions, and game-based security proofs can be formalized using the CryptHOL framework. As a running example, we formalize a variant of the hash-based ElGamal encryption scheme and its IND-CPA security in the random oracle model. This tutorial assumes familiarity with Isabelle/HOL basics and standard cryptographic terminology.

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

Date: received 3 Oct 2018

Contact author: mail at andreas-lochbihler de

Available format(s): PDF | BibTeX Citation

Note: This paper explains how to use the CryptHOL framework to formalize game-based security proofs. It complements the theoretical CryptHOL paper (e-print 2017/753), which focues on the theoretical foundations.

Version: 20181005:131724 (All versions of this report)

Short URL: ia.cr/2018/941


[ Cryptology ePrint archive ]