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].

[1]

A. V. Hess, S. Mödersheim, A. D. Brucker, and A. Schlichtkrull, “Automated stateful protocol verification,” *Archive of Formal Proofs*, Apr. 2020,

[2]

A. V. Hess, S. Mödersheim, and A. D. Brucker, “Stateful protocol composition and typing,” *Archive of Formal Proofs*, Apr. 2020,

[3]

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.

[4]

A. V. Hess, S. Mödersheim, A. D. Brucker, and A. Schlichtkrull, “Performing security proofs of stateful protocols,” in *34th IEEE computer security foundations symposium (CSF)*, 2021, vol. 1, pp. 143–158. doi: 10.1109/CSF51468.2021.00006.

[5]

A. V. Hess, S. A. Mödersheim, and A. D. Brucker, “Stateful protocol composition in isabelle/HOL,” *ACM Transactions on Privacy and Security*, 2023,