PSPSP: Performing Security Proofs of Stateful Protocols
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.
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.
This work is part of an Isabelle formalization of stateful protocols
where you can also manually reason about protocols and their composition.
The verification idea was previously implemented in Set-based abstraction:
AIF, Set-pi and AIF-Omega (Set-based abstraction)