The formal analysis of security protocols is dominated by automated protocol verification tools. They are based on abstract interpretation techniques and other over-approximations and their implementations are highly optimized and complex.

Such a complex verification tool may suffer from bugs resulting in accepting some incorrect protocols as 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.

To address these problems, we work on combining 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.

Our formalization and our tool PSPSP are published and maintained in the Archive of Formal Proofs (AFP) [1], [2].

Important Publications