Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL
David Basin, Andreas Lochbihler, Ueli Maurer, and S. Reza Sefidgar
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.
BibTeX Citation
@inproceedings{BLMS21,
author = {David Basin and Andreas Lochbihler and Ueli Maurer and S. Reza Sefidgar},
title = {Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL},
booktitle = {Computer Security Foundations Symposium -- CSF 2021},
pages = {1--16},
year = {2021},
}