Integrating Automated and Interactive Protocol Verification

@Unpublished{ talk:brucker.ea:integrating:2009-b,
  date       = {2009-12-09},
  title      = {Integrating Automated and Interactive Protocol Verification},
  month      = {dec},
  language   = {USenglish},
  venue      = {Saarbr{\"u}cken, Germany},
  author     = {Achim D. Brucker},
  eventtitle = {Computer Science Colloquium at the {German Research Center
                for Artificial Intelligence} ({DFKI})},
  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-approximated 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.},
  areas      = {formal methods, security},
  note       = {Author copy: \url{http://logicalhacking.com/publications/talk-brucker.ea-integrating-2009-b/}},
}