Automated Stateful Protocol Verification

 

Title: Automated Stateful Protocol Verification
Authors: Andreas V. Hess (avhe /at/ dtu /dot/ dk), Sebastian Mödersheim, Achim D. Brucker and Anders Schlichtkrull
Submission date: 2020-04-08
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.
BibTeX:
@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   = apr,
  year    = 2020,
  note    = {\url{http://isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Stateful_Protocol_Composition_and_Typing