Visible to the public Biblio

Filters: Keyword is proof rules  [Clear All Filters]
2020-09-14
Lochbihler, Andreas, Sefidgar, S. Reza, Basin, David, Maurer, Ueli.  2019.  Formalizing Constructive Cryptography using CryptHOL. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :152–15214.
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.