Paper 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.

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.