Local mirror of Automated Stateful Protocol Verification entry of the Archive of Formal Proofs (AFP).
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

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},
}