# Information Security and Cryptography Research Group

## Formalizing Constructive Cryptography using CryptHOL

### Andreas Lochbihler, S. Reza Sefidgar, David Basin, and Ueli Maurer

IEEE 32rd Computer Security Foundations Symposium (CSF), IEEE Press, Jun 2019.

Computer-aided cryptography increases the rigour of cryptographic proofs by mechanizing their verification. Ex- isting tools focus mainly on game-based proofs, and efforts to formalize composable frameworks such as Universal Composabil- ity have met with limited success. In this paper, we formalize an instance of Constructive Cryptography, a generic theory allowing for clean, composable cryptographic security statements. Namely, we extend CryptHOL, a framework for game-based proofs, with an abstract model of Random Systems and provide proof rules for their equality and composition. We formalize security as a special kind of system construction in which a complex system is built from simpler ones. As a simple case study, we formalize the construction of an information-theoretically secure channel from a key, a random function, and an insecure channel.

## BibTeX Citation

@inproceedings{LSBM19,
author       = {Andreas Lochbihler, S. Reza Sefidgar, David Basin, and Ueli Maurer},
title        = {Formalizing Constructive Cryptography using CryptHOL},
booktitle    = {IEEE 32rd Computer Security Foundations Symposium (CSF)},
year         = 2019,
month        = 6,
publisher    = {IEEE Press},
}