Integrating Automated and Interactive Protocol Verification

By Achim D. Brucker and Sebastian A. Mödersheim.

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.

Keywords:
Protocol Verification, Model-Checking, Theorem Proving

Supplementary material:
[ Slides Implementation  ]

Extended by:
An extended version is available as:
A. D. Brucker and S. A. Mödersheim, “Integrating automated and interactive protocol verification (extended version),” IBM Research Zurich, RZ3750, 2009. Author copy: https://logicalhacking.com/publications/brucker.ea-integrating-2009-b/

Please cite this work as follows:
A. D. Brucker and S. A. Mödersheim, “Integrating automated and interactive protocol verification,” in Workshop on formal aspects in security and trust (FAST 2009), P. Degano and J. Guttman, Eds. Heidelberg: Springer-Verlag, 2009, pp. 248–262. doi: 10.1007/978-3-642-12459-4_18. An extended version of this paper is available as IBM Research Technical Report, RZ3750.. Author copy: https://logicalhacking.com/publications/brucker.ea-integrating-2009/

BibTeX
@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},
  pages           = {248--262},
  doi             = {10.1007/978-3-642-12459-4_18},
  editor          = {Pierpaolo Degano and Joshua Guttman},
  year            = {2009},
  keywords        = {Protocol Verification, Model-Checking, Theorem Proving},
  areas           = {security, formal methods},
  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.},
  note            = {An extended version of this paper is available as IBM
                     Research Technical Report, RZ3750.. 
                     Author copy: \url{https://logicalhacking.com/publications/brucker.ea-integrating-2009/}},
  extendedby      = {brucker.ea:integrating:2009-b},
  supplementary01 = {https://git.logicalhacking.com/ProtocolSecurity/isabelle-ofmc},
  supplabel01     = {Implementation},
  pdf             = {https://logicalhacking.com/publications/brucker.ea-integrating-2009/brucker.ea-integrating-2009.pdf},
}