Automated Stateful Protocol Verification

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

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.

Please cite this work as follows:
A. V. Hess, S. Mödersheim, A. D. Brucker, and A. Schlichtkrull, “Automated stateful protocol verification,” Archive of Formal Proofs, Apr. 2020. https://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html, Formal proof development. Author copy: http://logicalhacking.com/publications/hess.ea-automated-2020/

BibTeX
@Article{ hess.ea:automated:2020,
  author    = {Andreas V. Hess and Sebastian M{\"o}dersheim and Achim D.
               Brucker and Anders Schlichtkrull},
  title     = {Automated Stateful Protocol Verification},
  journal   = {Archive of Formal Proofs},
  month     = {apr},
  year      = {2020},
  date      = {2020-04-08},
  note      = {\url{https://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html},
               Formal proof development. 
               Author copy: \url{http://logicalhacking.com/publications/hess.ea-automated-2020/}},
  issn      = {2150-914x},
  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.},
  filelabel = {Outline},
  file      = {download/2020/hess.ea-automated-outline-2020.pdf},
  areas     = {formal methods, security},
}