Automated Stateful Protocol Verification

Title:	Automated Stateful Protocol Verification
Authors:	Andreas V. Hess (avhe /at/ dtu /dot/ dk), Sebastian Mödersheim, Achim D. Brucker (a /dot/ brucker /at/ exeter /dot/ ac /dot/ uk) 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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.