Automated Stateful Protocol Verification

Andreas V. Hess 📧, Sebastian Mödersheim 🌐, Achim D. Brucker 🌐 and Anders Schlichtkrull 🌐

April 8, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. In this AFP entry, we present a fully-automated approach for verifying stateful security protocols, i.e., protocols with mutable state that may span several sessions. The approach supports reachability goals like secrecy and authentication. We also include a simple user-friendly transaction-based protocol specification language that is embedded into Isabelle.


BSD License


Session Automated_Stateful_Protocol_Verification