This is a developer release for Isabelle/OFMC, i.e., while it may be of interested to experts, it is not yet useable by the general public. This development version comprise a small Isabelle theory and a prototypical tool, called anb2thy. Using OFMC's fixed-point module, anb2thy generate a Isabelle theory (for Isabelle 2016) file for protocols that haven been successfully validated by OFMC.
This project has been superseded by Automated Stateful Protocol Verification and is no longer maintained. In contrast, Automated Stateful Protocol Verification is actively maintained and also, as official entry of the Archive of Formal Proofs, always supports the latest version of Isabelle. More information about the Automated Stateful Protocol Verification project (including its source code) is available in the AFP:
- Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull. Automated Stateful Protocol Verification. In Archive of Formal Proofs, 2020. http://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html, Formal proof development.
The following publication provides a more abstract description of the underlying theory:
- Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull. Performing Security Proofs of Stateful Protocols. In 34th IEEE Computer Security Foundations Symposium (CSF). IEEE, 2021. doi:10.1109/CSF51468.2021.00006. https://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019
This project is licensed under a 2-clause BSD-style license.
SPDX-License-Identifier: BSD-2-Clause
The master git repository for this project is hosted by the Software Assurance & Security Research Team at https://git.logicalhacking.com/ProtocolSecurity/isabelle-ofmc.
- Achim D. Brucker and Sebastian A. Mödersheim. Integrating Automated and Interactive Protocol Verification. In Workshop on Formal Aspects in Security and Trust (FAST 2009). Lecture Notes in Computer Science (5983), pages 248-262, Springer-Verlag , 2009. https://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009. doi: 10.1007/978-3-642-12459-4_18