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