About the Tool

This tool is the first to combine three things:

• Machine-checked security proofs in Isabelle/HOL
  This gives the high assurance that a positive result is not due to a bug in the tool: the proof is checked by Isabelle/HOL, thus relying on a small trusted code base.
• Fully automated verification
  PSPSP is based on an abstract interpretation approach: it computes a fixed-point that over-approximates what can ever happen in the protocol. Isabelle then checks that indeed nothing else can happen in the real protocol. This entire process is automatic and does not require any user guidance.
• Stateful Protocols
  We support stateful protocols, i.e., where participants have a long-term state such as a server database. This allows us to go beyond simple protocols of isolated sessions.

Download

• Tool:
  • New release under development
  • Stable version as part of the AFP
  • Previous Version
• Papers:
  • Andreas Hess, Sebastian Mödersheim, Achim Brucker, and Anders Schlichtkrull: PSPSP: A Tool for Automated Verification of Stateful Protocols in Isabelle/HOL, JCS 2025, to appear. Preprint
  • Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull: Performing Security Proofs of Stateful Protocols. CSF 2021 Preprint and CSF article

Composition

This work is part of an Isabelle formalization of stateful protocols where you can also manually reason about protocols and their composition.

Related tools

The verification idea was previously implemented in Set-based abstraction:
AIF, Set-pi and AIF-Omega (Set-based abstraction)