PSPSP: A Tool for Automated Verification of Stateful Protocols in Isabelle/HOL

By Andreas Viktor Hess, Sebastian Alexander Mödersheim, Achim D. Brucker, and Anders Schlichtkrull.

In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide 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 non-negligible. There are a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step towards 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 soundness of a typed model.

Keywords:
Formal Verification, Theorem Proving, Security Protocols

Please cite this work as follows:
A. V. Hess, S. A. Mödersheim, A. D. Brucker, and A. Schlichtkrull, “PSPSP: A tool for automated verification of stateful protocols in Isabelle/HOL,” Journal of Computer Security, vol. 33, Nov. 2025, doi: 10.1177/0926227X251358741.

BibTeX
@Article{ hess.ea:pspsp:2025,
  author    = {Andreas Viktor Hess and Sebastian Alexander M{\"o}dersheim
               and Achim D. Brucker and Anders Schlichtkrull},
  journal   = {Journal of Computer Security},
  publisher = {IOS Press},
  language  = {USenglish},
  title     = {{PSPSP:} A Tool for Automated Verification of Stateful
               Protocols in {Isabelle/HOL}},
  year      = {2025},
  areas     = {security, formal methods},
  month     = {nov},
  volume    = {33},
  issue     = {6},
  doi       = {10.1177/0926227X251358741},
  keywords  = {Formal Verification, Theorem Proving, Security Protocols},
  abstract  = {In protocol verification we observe a wide spectrum from
               fully automated methods to interactive theorem proving with
               proof assistants like Isabelle/HOL. The latter provide
               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
               non-negligible. There are a few works that try to combine
               advantages from both ends of the spectrum: a high degree of
               automation and assurance. We present here a first step towards
               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 soundness of a typed
               model.},
}