| Title | Formalizing Constructive Cryptography using CryptHOL |
| Publication Type | Conference Paper |
| Year of Publication | 2019 |
| Authors | Lochbihler, Andreas, Sefidgar, S. Reza, Basin, David, Maurer, Ueli |
| Conference Name | 2019 IEEE 32nd Computer Security Foundations Symposium (CSF) |
| Date Published | jun |
| Keywords | complex system, Complexity theory, composability, composable cryptographic security statements, computer aided cryptography, Computer science, computer-aided cryptography, constructive cryptography, CryptHOL, cryptographic proofs, cryptography, Encryption, formal methods, formal verification, game theory, game-based proofs, information-theoretically secure channel, Probabilistic logic, proof rules, pubcrawl, random systems, theorem proving, Tools, universal composability, verification |
| Abstract | Computer-aided cryptography increases the rigour of cryptographic proofs by mechanizing their verification. Existing tools focus mainly on game-based proofs, and efforts to formalize composable frameworks such as Universal Composability 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. |
| DOI | 10.1109/CSF.2019.00018 |
| Citation Key | lochbihler_formalizing_2019 |
Formalizing Constructive Cryptography using CryptHOL