Performing Security Proofs of Stateful Protocols

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

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

1 Downloads (Pure)


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
Titel2021 IEEE 34th Computer Security Foundations Symposium (CSF)
Antal sider16
ISBN (Trykt)978-1-7281-7608-6
ISBN (Elektronisk)978-1-7281-7607-9
StatusUdgivet - 2021
Begivenhed 2021 IEEE 34th Computer Security Foundations Symposium (CSF) -
Varighed: 21 jun. 202125 jun. 2021


Konference 2021 IEEE 34th Computer Security Foundations Symposium (CSF)
NavnProceedings of the IEEE Computer Security Foundations Symposium


Dyk ned i forskningsemnerne om 'Performing Security Proofs of Stateful Protocols'. Sammen danner de et unikt fingeraftryk.