ETH Zürich » Computer Science » Theory » Cryptography

Publications: Abstract

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.