You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
69 lines
4.0 KiB
69 lines
4.0 KiB
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},
|
|
}
|