Formal Verification of Composable Security Proofs
OPEN ACCESS
Author / Producer
Date
2021
Publication Type
Doctoral Thesis
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Computer-aided cryptography improves the rigor of security proofs by mechanizing their verification. Existing formal-methods tools focus primarily on the game-based paradigm, and the results on formalizing simulation-based proofs are limited. Simulation-based frameworks are popular since they support the composition of security proofs, but the level of details in these frameworks surpasses what the formal-methods community can reasonably handle with state-of-the-art techniques. Hence, existing formal results consider streamlined versions of simulation-based frameworks to cope with their complexity.
Recent advancements in cryptography frameworks enable the development of better tools for formalizing composable security proofs. Constructive Cryptography is a generic theory allowing for clean, composable security statements that empowers protocol designers to focus on a particular aspect of security proofs without being distracted by other details.
It lays the foundation for formal-methods tools that support mechanized verification of composable security statements.
In this thesis, we formalize an instance of Constructive Cryptography. Our approach is suitable for mechanized verification and we use CryptHOL, a framework for developing mechanized cryptography proofs, to implement it in the Isabelle/HOL theorem prover. We extend CryptHOL with an abstract model of Random Systems and provide proof rules for their equality and composition. We then formalize security as a special kind of random system construction in which a complex system is built from simpler ones. We demonstrate the practicality of our approach by formalizing two different constructions of a secure channel.
Our formal approach enables us to delve into an aspect of composable security proofs that has not been considered in previous formal results: we highlight the importance of system communication modeling in composable security statements. We show that fixing the communication patterns, which is sometimes applied to simplify proofs and overcome their complexity, can affect the reusability of security statements. We propose an abstract approach to modeling systems communication in Constructive Cryptography that avoids this problem.
Permanent link
Publication status
published
External links
Editor
Contributors
Examiner : Basin, David
Examiner : Maurer, Ueli
Examiner : Barthe, Gilles
Examiner : Lochbihler, Andreas
Book title
Journal / series
Volume
Pages / Article No.
Publisher
ETH Zurich
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Formal methods; Cryptography; Security; Theorem proving
Organisational unit
03634 - Basin, David / Basin, David