# Constructive Cryptography in HOL

 Title: Constructive Cryptography in HOL Authors: Andreas Lochbihler and S. Reza Sefidgar Submission date: 2018-12-17 Abstract: 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. BibTeX: @article{Constructive_Cryptography-AFP, author = {Andreas Lochbihler and S. Reza Sefidgar}, title = {Constructive Cryptography in HOL}, journal = {Archive of Formal Proofs}, month = dec, year = 2018, note = {\url{http://isa-afp.org/entries/Constructive_Cryptography.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: CryptHOL Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.