AnBx IDE

This Integrated Development Environment (IDE) facilitates the design, verification, and implementation of security protocols, aiming to reduce the adoption barrier for formal methods tools in the security domain. Following the principles of Model-Driven Development (MDD), the environment assists users in specifying models with the simple and intuitive Alice and Bob (AnB) narration language, as well as its extension, AnBx. Additionally, it offers a push-button solution for the formal verification of both abstract and concrete models, and the automatic generation of Java implementations and ProVerif specifications. The tool also supports the applied pi calculus, used for modelling security protocols in ProVerif.

Key Features:

This Eclipse-based IDE integrates with existing languages and tools for the modelling and verification of security protocols, including:

• AnBx Compiler and Code Generator: Targets include AnB, ProVerif, Java, and Java (Docker).
• OFMC: A model checker, for security protocols verification.
• ProVerif: A verifier for cryptographic protocols.

Requirements:

• Java 17 or later.
• XText Redistributable 2.34.0 or later.
• External tools (AnBx Compiler, OFMC, and ProVerif) need to be downloaded separately. Packages for Windows, Linux, and macOS are available on the support site, where you will also find comprehensive documentation.