@inproceedings{f4f8791ff0804e3083cdc69a214f8926,
title = "Performing Security Proofs of Stateful Protocols",
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",
author = "Hess, {Andreas V.} and Sebastian M{\"o}dersheim and Brucker, {Achim D.} and Anders Schlichtkrull",
year = "2021",
doi = "10.1109/CSF51468.2021.00006",
language = "English",
isbn = "978-1-7281-7608-6",
series = "Proceedings of the IEEE Computer Security Foundations Symposium",
publisher = "IEEE",
pages = "1--16",
booktitle = "2021 IEEE 34th Computer Security Foundations Symposium (CSF)",
address = "United States",
note = "null ; Conference date: 21-06-2021 Through 25-06-2021",
}