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.

References

1. Hess, A. V., Mödersheim, S., Brucker, A. D., and Schlichtkrull, A. “Performing Security Proofs of Stateful Protocols34th IEEE computer security foundations symposium (csf) 1, (2021): 143–158. doi:10.1109/CSF51468.2021.00006, URL: http://www.brucker.ch/bibliography/abstract/hess.ea-performing-2021

2. Hess, A. V., Mödersheim, S., Brucker, A. D., and Schlichtkrull, A. “Automated Stateful Protocol VerificationArchive of Formal Proofs (2020): URL: http://www.brucker.ch/bibliography/abstract/hess.ea-automated-2020