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

    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},

Files and Links