Automated stateful protocol verification
Hess, AV; Mödersheim, S; Brucker, AD; et al.Schlichtkrull, A
Date: 8 April 2020
Journal
Archive of Formal Proofs
Publisher
AFP
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 ...
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.
Computer Science
Faculty of Environment, Science and Economy
Item views 0
Full item downloads 0