PSPSP: A tool for automated verification of stateful protocols in Isabelle/HOL

In protocol verification, we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants such as Isabelle/HOL. The latter provides overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely, and thus the risk of erroneously verifying a flawed protocol is nonnegligible. There are a few works that try to combine the advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step toward achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge, this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results, such as the soundness of a typed model.