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.

Abstract

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.

License

BSD License

Topics

Related publications

  • Hess, A. V., Mödersheim, S. A., Brucker, A. D., & Schlichtkrull, A. (2025). PSPSP: A tool for automated verification of stateful protocols in Isabelle/HOL. Journal of Computer Security, 33(6), 425–469. https://doi.org/10.1177/0926227x251358741

Session Automated_Stateful_Protocol_Verification

Depends on

Cite

× 
@article{Automated_Stateful_Protocol_Verification-AFP,
  author  = {Andreas V. Hess and Sebastian Mödersheim and Achim D. Brucker and Anders Schlichtkrull},
  title   = {Automated Stateful Protocol Verification},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: