### 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

- Computer science/Security
- Tools

### Session Automated_Stateful_Protocol_Verification

- Transactions
- Term_Abstraction
- Stateful_Protocol_Model
- Term_Variants
- Term_Implication
- Stateful_Protocol_Verification
- Eisbach_Protocol_Verification
- ml_yacc_lib
- trac_term
- trac_fp_parser
- trac_protocol_parser
- trac
- PSPSP
- introduction
- KeyserverEx
- manual
- Keyserver
- Keyserver2
- Keyserver_Composition
- PKCS_Model03
- PKCS_Model07
- PKCS_Model09
- Examples

### Depends on

- Stateful Protocol Composition and Typing

### Auto-related entries

- S-Finite Measure Monad on Quasi-Borel Spaces
- Proof Strategy Language

## Cite

×

Automated_Stateful_Protocol_Verification-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- May 20, 2020 : Isabelle2020