Title: Formalizing Constructive Cryptography using CryptHOL

Abstract: Computer-aided cryptography increases the rigour of cryptographic proofs by mechanizing their verification. Existing tools focus mainly on game-based proofs, and efforts to formalize composable frameworks such as Universal Composability have met with limited success. I present our formalization of Constructive Cryptography, a generic theory allowing for clean, composable cryptographic security statements. I explain how we extened CryptHOL, a framework for game-based proofs in Isabelle/HOL, to make such a formalization feasible. The extended framework allows one to formalize security as a special kind of system construction in which a complex system is built from simpler ones. As a running example, I will demonsterate the formalized construction of an information-theoretically secure channel from a key, a random function, and an insecure channel.

Speaker: Seyed Reza Sefidgar from ETH Zürich 

About: The talk is open to everyone and is organized by the Concordium Blockchain Research Center Aarhus. For further information about the research center please visit the center website: http://cs.au.dk/research/centers/concordium/