TY - CHAP AU - Brucker, Achim D. AU - Mödersheim, Sebastian A. ED - Degano, Pierpaolo ED - Guttman, Joshua PY - 2009 DA - 2009// TI - Integrating Automated and Interactive Protocol Verification BT - Workshop on Formal Aspects in Security and Trust (FAST 2009) T3 - Lecture Notes in Computer Science SP - 248 EP - 262 IS - 5983 PB - Springer-Verlag CY - Heidelberg KW - protocol verification, model-checking, theorem proving AB - 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. L1 - https://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009.pdf L1 - https://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009-b.pdf UR - https://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009 UR - https://doi.org/10.1007/978-3-642-12459-4_18 DO - 10.1007/978-3-642-12459-4_18 N1 - An extended version of this paper is available as IBM Research Technical Report, RZ3750. ID - brucker.ea:integrating:2009 ER -