Constructive Cryptography in HOL

Andreas Lochbihler 🌐 and S. Reza Sefidgar

December 17, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Inspired by Abstract Cryptography, we extend CryptHOL, a framework for formalizing game-based proofs, with an abstract model of Random Systems and provide proof rules about their composition and equality. This foundation facilitates the formalization of Constructive Cryptography proofs, where the security of a cryptographic scheme is realized as a special form of construction in which a complex random system is built from simpler ones. This is a first step towards a fully-featured compositional framework, similar to Universal Composability framework, that supports formalization of simulation-based proofs.


BSD License


Session Constructive_Cryptography