Posted on by Achim D. Brucker, licensed under CC BY-ND 4.0.

Performing Security Proofs of Stateful Protocols

In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely and thus the risk of erroneously verifying a flawed protocol is non-negligible. There are a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance.

In our CSF paper [1], we present here a first step towards achieving this for a more challenging class of protocols, namely those that work with a mutable long- term state. To our knowledge this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results such as soundness of a typed model.

The formalization and the automated tool PSPSP [2] are available in the Archive of Formal Proofs.


A. V. Hess, S. Mödersheim, A. D. Brucker, and A. Schlichtkrull, “Performing security proofs of stateful protocols,” in 34th IEEE computer security foundations symposium (CSF), 2021, vol. 1, pp. 143–158. doi: 10.1109/CSF51468.2021.00006.
A. V. Hess, S. Mödersheim, A. D. Brucker, and A. Schlichtkrull, Automated stateful protocol verification,” Archive of Formal Proofs, Apr. 2020,

Welcome to the blog of the Software Assurance & Security Research Team at the University of Exeter. We blog regularly news, tips & tricks, as well as fun facts about software assurance, reliability, security, testing, verification, hacking, and logic.

You can also follow us on Twitter: @logicalhacking.




academia ai android apidesign appsec bitcoin blockchain bpmn browser browserextensions browsersecurity bug certification chrome composition cordova dast devops devsecops dom dsbd efsm epsrc event extensions fixeffort floss formaldocument formalmethods funding hol-ocl hol-testgen humanfactor hybridapps iast industry internetofthings iot isabelle/hol isabelledof isadof latex logic maintance malicous mbst mobile mobile apps modelinference modeling monads monitoring msc ocl ontology opensource owasp patches pet phd phdlife phishing policy protocols publishing reliability research safelinks safety sap sast sdlc secdevops secureprogramming security securityengineering securitytesting semantics servicecomposition skills smartcontract smartthings softwareeinginering softwaresecurity softwaresupplychain solidity staff&positions statemachine studentproject tcb test&proof testing tips&tricks tools transport tuos uk uoe upgrade usability verification vulnerabilities vulnerableapplication webinar websecurity


blog whole site