@TechReport{ brucker.ea:integrating:2009-b,
title = {Integrating Automated and Interactive Protocol Verification (Extended Version)},
author = {Achim D. Brucker and Sebastian A. M{\"o}dersheim},
year = {2009},
classification= {unrefereed},
categories = {isabelleofmc},
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-b.pdf},
number = {RZ3750},
institution = {IBM Research Zurich},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009-b}
}