| Title | Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL |
| Publication Type | Conference Paper |
| Year of Publication | 2021 |
| Authors | Basin, David, Lochbihler, Andreas, Maurer, Ueli, Sefidgar, S. Reza |
| Conference Name | 2021 IEEE 34th Computer Security Foundations Symposium (CSF) |
| Date Published | jun |
| Keywords | Complexity theory, composability, Computational modeling, computer security, cryptography, pubcrawl, Tools |
| Abstract | Proofs in simulation-based frameworks have the greatest rigor when they are machine checked. But the level of details in these proofs surpasses what the formal-methods community can handle with existing tools. Existing formal results consider streamlined versions of simulation-based frameworks to cope with this complexity. Hence, a central question is how to abstract details from composability results and enable their formal verification.In this paper, we focus on the modeling of system communication in composable security statements. Existing formal models consider fixed communication patterns to reduce the complexity of their proofs. However, as we will show, this can affect the reusability of security statements. We propose an abstract approach to modeling system communication in Constructive Cryptography that avoids this problem. 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. As a case study, we formalize the construction of a secure channel using Diffie-Hellman key exchange and a one-time-pad. |
| DOI | 10.1109/CSF51468.2021.00047 |
| Citation Key | basin_abstract_2021 |
Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL