Formalizing Constructive Cryptography using CryptHOL
Andreas Lochbihler, S. Reza Sefidgar, David Basin, and Ueli Maurer
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},
}