Isabelle/OFMC - Linking OFMC and Isabelle/HOL
https://www.brucker.ch/projects/isabelle-ofmc/
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.
60 lines
2.8 KiB
60 lines
2.8 KiB
To cite ofmc-isabelle, please use
|
|
|
|
Achim D. Brucker and Sebastian A. Mödersheim. Integrating Automated
|
|
and Interactive Protocol Verification. In Workshop on Formal Aspects
|
|
in Security and Trust (FAST 2009). Lecture Notes in Computer Science (5983),
|
|
pages 248-262, Springer-Verlag , 2009.
|
|
doi: 10.1007/978-3-642-12459-4_18
|
|
|
|
A BibTeX entry for LaTeX users is
|
|
|
|
@InCollection{ brucker.ea:integrating:2009,
|
|
title = {Integrating Automated and Interactive Protocol
|
|
Verification},
|
|
author = {Achim D. Brucker and Sebastian A. M{\"o}dersheim},
|
|
booktitle = {Workshop on Formal Aspects in Security and Trust (FAST
|
|
2009)},
|
|
publisher = {Springer-Verlag},
|
|
address = {Heidelberg},
|
|
series = {Lecture Notes in Computer Science},
|
|
number = {5983},
|
|
categories = {isabelleofmc},
|
|
pages = {248--262},
|
|
doi = {10.1007/978-3-642-12459-4_18},
|
|
editor = {Pierpaolo Degano and Joshua Guttman},
|
|
year = {2009},
|
|
classification= {workshop},
|
|
keywords = {protocol verification, model-checking, theorem proving},
|
|
areas = {security, formal methods},
|
|
public = {yes},
|
|
abstract = {A number of current automated protocol verification tools
|
|
are based on abstract interpretation techniques and other
|
|
over-approximations of the set of reachable states or
|
|
traces. The protocol models that these tools employ are
|
|
shaped by the needs of automated verification and require
|
|
subtle assumptions. Also, a complex verification tool may
|
|
suffer from implementation bugs so that in the worst case
|
|
the tool could accept some incorrect protocols as being
|
|
correct. These risks of errors are also present, but
|
|
considerably smaller, when using an LCF-style theorem
|
|
prover like Isabelle. The interactive security proof,
|
|
however, requires a lot of expertise and time.
|
|
|
|
We combine the advantages of both worlds by using the
|
|
representation of the over-approx\-imated search space
|
|
computed by the automated tools as a ``proof idea'' in
|
|
Isabelle. Thus, we devise proof tactics for Isabelle that
|
|
generate the correctness proof of the protocol from the
|
|
output of the automated tools. In the worst case, these
|
|
tactics fail to construct a proof, namely when the
|
|
representation of the search space is for some reason
|
|
incorrect. However, when they succeed, the correctness only
|
|
relies on the basic model and the Isabelle core.},
|
|
pdf = {https://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009.pdf},
|
|
note = {An extended version of this paper is available as IBM
|
|
Research Technical Report, RZ3750.},
|
|
filelabel = {Extended Version},
|
|
file = {https://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009-b.pdf},
|
|
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009}
|
|
}
|
|
|
|
|