Performing Security Proofs of Stateful Protocols

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

Cover for hess.ea:performing:2021.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.

Schlüsselwörter:
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for hess.ea:performing:2021.Bitte zitieren sie diesen Artikel wie folgt:
Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker und Anders Schlichtkrull. Performing Security Proofs of Stateful Protocols. In 34th IEEE Computer Security Foundations Symposium (CSF). , 1, pages 143-158, IEEE, 2021.
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1109/CSF51468.2021.00006) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InProceedings{ hess.ea:performing:2021,
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 = {Andreas V. Hess and Sebastian M{\"o}dersheim and Achim D. Brucker and Anders Schlichtkrull},
booktitle = {34th {IEEE} Computer Security Foundations Symposium (CSF)},
doi = {10.1109/CSF51468.2021.00006},
location = {June 21-25, 2021, Dubrovnik, Croatia},
pages = {143--158},
pdf = {https://www.brucker.ch/bibliography/download/2021/hess.ea-performing-2021.pdf},
publisher = {{IEEE}},
title = {Performing Security Proofs of Stateful Protocols},
url = {https://www.brucker.ch/bibliography/abstract/hess.ea-performing-2021},
volume = {1},
year = {2021},
}