@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.},
}