| Title | Performing Security Proofs of Stateful Protocols |
| Publication Type | Conference Paper |
| Year of Publication | 2021 |
| Authors | Hess, Andreas V., Mödersheim, Sebastian, Brucker, Achim D., Schlichtkrull, Anders |
| Conference Name | 2021 IEEE 34th Computer Security Foundations Symposium (CSF) |
| Keywords | automated-verification, Automation, Collaboration, Complexity theory, composability, compositionality, Computational modeling, Computer bugs, interactive-theorem-proving, policy-based collaboration, privacy, protocol verification, Protocols, pubcrawl, specification languages, stateful-security-protocols, Tools |
| Abstract | In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely and thus the risk of erroneously verifying a flawed protocol is non-negligible. There are a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step towards achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results such as soundness of a typed model |
| DOI | 10.1109/CSF51468.2021.00006 |
| Citation Key | hess_performing_2021 |
Performing Security Proofs of Stateful Protocols