Automated Stateful Protocol Verification (Q7361464)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Automated_Stateful_Protocol_Verification
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Automated Stateful Protocol Verification |
AFP entry Automated_Stateful_Protocol_Verification |
Statements
8 April 2020
0 references
Andreas V. Hess
0 references
Sebastian Mödersheim
0 references
Achim D. Brucker
0 references
Anders Schlichtkrull
0 references
Automated Stateful Protocol Verification (English)
0 references
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.
0 references
