Performing Security Proofs of Stateful Protocols

By Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull.

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

Supplementary material:
[  Formalization and Tool  ]

Please cite this work as follows:
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. Author copy: http://logicalhacking.com/publications/hess.ea-performing-2021/

BibTeX
@InProceedings{ hess.ea:performing:2021,
  author          = {Andreas V. Hess and Sebastian M{\"o}dersheim and Achim D.
                     Brucker and Anders Schlichtkrull},
  title           = {Performing Security Proofs of Stateful Protocols},
  booktitle       = {34th {IEEE} Computer Security Foundations Symposium (CSF)},
  publisher       = {{IEEE}},
  year            = {2021},
  pages           = {143--158},
  volume          = {1},
  doi             = {10.1109/CSF51468.2021.00006},
  areas           = {formal methods, security},
  location        = {June 21-25, 2021, Dubrovnik, Croatia},
  abstract        = {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. 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.},
  supplementary01 = {https://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html},
  supplabel01     = {Formalization and Tool},
  note            = {Author copy: \url{http://logicalhacking.com/publications/hess.ea-performing-2021/}},
}