Performing Security Proofs of Stateful Protocols

Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, Anders Schlichtkrull

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

1 Citation (Scopus)
24 Downloads (Pure)


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
Original languageEnglish
Title of host publication2021 IEEE 34th Computer Security Foundations Symposium (CSF)
Number of pages16
Publication date2021
Article number9505200
ISBN (Print)978-1-7281-7608-6
ISBN (Electronic)978-1-7281-7607-9
Publication statusPublished - 2021
Event 2021 IEEE 34th Computer Security Foundations Symposium (CSF) -
Duration: 21 Jun 202125 Jun 2021


Conference 2021 IEEE 34th Computer Security Foundations Symposium (CSF)
SeriesProceedings of the IEEE Computer Security Foundations Symposium


Dive into the research topics of 'Performing Security Proofs of Stateful Protocols'. Together they form a unique fingerprint.

Cite this