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.