Treffer: PSPSP: A tool for automated verification of stateful protocols in Isabelle/HOL.

In protocol verification, we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants such as Isabelle/HOL. The latter provides 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 nonnegligible. There are a few works that try to combine the advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step toward 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 the soundness of a typed model. [ABSTRACT FROM AUTHOR]

Copyright of Journal of Computer Security is the property of Sage Publications Inc. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)