|
- To cite the use of this formal theory, please use
-
- Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull.
- Automated Stateful Protocol Verification. In Archive of Formal Proofs, 2020.
- http://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html,
- Formal proof development
-
- A BibTeX entry for LaTeX users is
-
- Article{ hess.ea:automated:2020,
- abstract= {In protocol verification we observe a wide spectrum from fully
- automated methods to interactive theorem proving with proof
- assistants like Isabelle/HOL. In this AFP entry, we present a
- fully-automated approach for verifying stateful security protocols,
- i.e., protocols with mutable state that may span several sessions.
- The approach supports reachability goals like secrecy and
- authentication. We also include a simple user-friendly
- transaction-based protocol specification language that is embedded
- into Isabelle.},
- author = {Andreas V. Hess and Sebastian M{\"o}dersheim and Achim D. Brucker and Anders Schlichtkrull},
- date = {2020-04-08},
- file = {https://www.brucker.ch/bibliography/download/2020/hess.ea-automated-outline-2020.pdf},
- filelabel= {Outline},
- issn = {2150-914x},
- journal = {Archive of Formal Proofs},
- month = {apr},
- note = {\url{http://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html}, Formal proof development},
- pdf = {https://www.brucker.ch/bibliography/download/2020/hess.ea-automated-2020.pdf},
- title = {Automated Stateful Protocol Verification},
- url = {https://www.brucker.ch/bibliography/abstract/hess.ea-automated-2020},
- year = {2020},
- }
-
- An overview of the formalization is given in:
-
- Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and
- Anders Schlichtkrull. Performing Security Proofs of Stateful
- Protocols. In 34th IEEE Computer Security Foundations Symposium
- (CSF). IEEE, 2021.
- https://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019
-
- A BibTeX entry for LaTeX users is
-
- @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)},
- location = {June 21-25, 2021, Dubrovnik, Croatia},
- 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},
- year = {2021},
- }
|