Formalisation of Cryptographic Proofs in Agda

Abstract

The game-based style of proofs [BR06, Sho04] is often used in cryptography to prove properties of cryptographic primitives, such as the security of an encryption scheme. Given the importance of cryptography in the modern world, there is considerable value in being able to verify these proofs automatically. In this thesis, we develop a system for expressing proofs of this form in the Agda programming language.