This is the Eclipse Update Site for the AnBx IDE

Authors: Rémi Garcia and Paolo Modesti

This plugin extends the Eclipse IDE for the design, verification and implementation of security protocols. It is aimed at lowering the adoption barrier of formal methods tools for security. In the spirit of Model Driven Development, the environment supports the user in the specification of the model using the simple and intuitive language Alice and Bob notation (AnB) (and its extension AnBx). Moreover, it provides a push-button solution for the formal verification of the abstract and concrete models, and for the automatic generation of Java implementation. The tools supports also the ProVerif tool and the applied-pi language.

Main features

• Input Languages: Security Protocols in Alice and Bob notation (AnBx and AnB), typed applied pi calculus (ProVerif), AVISPA IF (OFMC)
• Syntax Highlighting, Protocol Outline, Validation, Quick Fixes
• Back-end tools: AnBx compiler, OFMC, ProVerif
• Protocol verification/run, task manager, with output coloring:
  • OFMC: single/multiple sessions, single/multiple goals
  • ProVerif: automatic generation of applied pi specification from AnBx/AnB model, single/multiple goals
  • Java: automatic generation of Java code from AnBx/AnB model, local or distributed (Docker) execution
• AnBx IDE User Manual

Installation

The simplest way is to install the plugin is:

• Within Eclipse, select the Help menu -> Eclipse Marketplace... and search AnBx and press Enter. Select the AnBx IDE from the list and press Install (requires the Eclipse Marketplace to be active in Eclipse).
• Make sure the update site is active to receive future updates (check Help -> Install New Software... -> Manage... and double check the checkbox on the left of the update site is flagged on).
  
  Alternatively: Drag and drop the button on your Eclipse Workspace.

You can also install the plugin using the Eclipse Update Manager. To learn how to install software from an update site, please carefully read Adding a new software site from Eclipse Online-Help and follow the instructions there.
Use the following address https://paolo.science/anbx/ for the update site.

N.B. The current version of the AnBx IDE requires Java 17 or later. A recent version of Eclipse is recommended.

Backend Tools - Quick setup for Windows, Linux and Mac

For your convenience, we provide a zip file with executables, AnBxJ library and Java templates for the most popular Operating Systems:

• Windows (x64)
• Linux
• Mac (x64 and Arm64)

Unzip the package on a local folder of your system. In most cases, you will just need to configure the plugin in Eclipse.
On Mac and Linux you likely will need to set execution permission to the three binary files: anbxc, ofmc and proverif.
This can be done with the command chmod u+x filename or with the OS GUI. On Mac, you may also need to authorise the execution of the binary files in System Preferences -> Security and Privacy, go to General tab and click Allow.

The current version of the AnBx compiler is .
If the executables are outdated, or you are using another operating system, you will need to build your own executables.
For the procedure to build each tool refer to documentation of the package.

Download and installation of tools from source code

If you are not using any of the redistributable packages, the AnBx IDE requires to download and configure the following software:

• AnBx Compiler and Code Generator (standard distribution includes windows binaries)
• OFMC model checker (standard distribution includes win, linux and mac binaries)
• ProVerif protocol verifier (standard distribution includes only win binaries)

Configuration of the plugin

To configure the plugin, in Eclipse select AnBx Tools -> Configuration, and set the paths to the executables of these tools and to the config file anbxc.cfg.
In order to work with this plugin, if you have downloaded the zip file for win or mac with the executable and auxiliary files, you should set the following under AnBx Tools -> Configuration:

1. AnBxC Exe Path -> /AnBx2/bin/anbxc.exe
2. AnBxC Config File -> /AnBx2/bin/anbxc.cfg
3. AnBxC Exe Path -> /ext-tools/ofmc.exe
4. ProVerif Exe Path -> /ext-tools/proverif.exe

For each tool, the working directory is usually set one where the executable is located.
You can also, optionally, configure a folder for logging the output of tools. For each backend tool, you can enable/disable logging prior launching the tool.

For file with .java and .properties extensions, Eclipse will automatically use the most appropriate editor type (i.e. syntax highlighting and other features).
For the anbxc.cfg file you can enable syntax highlighting by right clicking on the file icon, and selecting "Open With" -> "Other..." -> "Properties File Editor". It is possible to make this selection permanent in the same dialog window.

Installation of Bouncy Castle library

The Bouncy Castle library offers support form many ciphers not included in the standard JDK/JRE. It can be configured as a Java cryptographic provider via static registration by adding an entry to the java.security properties file.
Download the "Provider" library file bcprov-jdk18on-.jar (or later) in the same folder containing the AnBxJ.jar file.
The file is in $JAVA_HOME/conf/security/java.security , where $JAVA_HOME is the location of your JDK/JRE distribution).
You basically need to add a line: security.provider.<n>=org.bouncycastle.jce.provider.BouncyCastleProvider
at the end of the list of other security providers and replace <n> with the next available integer (e.g. 14).
However, as recent versions of Eclipse ship a built-in JRE, you will also need to edit the java.security file, for that JRE.
To identify the location, in Eclipse, select Window -> Properties -> Java -> Installed JREs.

Working with existing examples and testing the environment configuration

If you want to check the configuration and experiment with the tools, the most convenient option is to:

• In Eclipse, click on File -> Open project from File System... Select the casestudies folder form the distribution file. The folder contains many AnBx protocols examples.
• In Eclipse, click on File -> Open project from File System... Select the genAnBx folder form the distribution file. The folder contains many generated Java protocols, from the AnBx examples.
  • Right click on the genAnBx folder, select Properties -> Java Build Path -> Libraries. Click on Classpath, and the on the Add External Jars... button. Select the AnBxJ.jar and Bouncy castle jar in the AnBxJ folder and click OK. Then Apply and Close
• Select now a protocol, for example Fresh_From_A.AnBx from the casestudies folder.
  • Click on the AnBxC button on the toolbar. Select as output format AnB and make sure the Launch associated validator is selected. Press OK. In the console(s), you should the result of the OFMC verification.
  • Repeat the above with the output format: ProVerif Typed. In the console(s), you will observe the ProVerif verification process and results.
  • Finally, run the output format: Java. In the console, you will observe the generated code and the application run. To make sure the code runs correctly on your machine, double check the parameters interface and ipaddress in your anbxc.cfg file. You will typically need to set just one of the two parameters. (Look at the comments in the anbxc.cfg file for details).

Creating a new project or file

1. Create a new AnBx project in Eclipse
   File -> New -> Project -> AnBx -> AnBx Project
2. Create your AnBx/AnB files inside the src folder of the project
   File -> New -> Others -> AnBx file
3. Create your PV files inside the src folder of the project
   File -> New -> Others -> PV file

Note that when you create the project a symbolic link to the configuration file anbxc.cfg is created.

Running the tool - Protocol verification and code generation

When you run the tool, the output will be displayed in the "Console". Be sure you select the right console in Eclipse.
At the first run of any supported tool a  console should open automatically. If you do not see any Console select Window -> Show View -> Console.

OFMC protocol verification (only for AnBx/AnB files)

1. If your input file has extension .AnBx
   1. Select your AnBx file and click on "AnBxC" button.
   2. Select the output format "AnB (default)" and select "Launch associated validator"
   3. (Only the first time) Configure OFMC (click on the "gear" icon): set the number of session (1,2,3...). If the number (n) is greater then one the tool will verify the protocol for 1 and n session in sequence.
   4. Click "OK". The compiler will translate the file from AnBx to AnB and will run OFMC to verify the protocol specification against the security goals.
2. If your input file has extension .AnB or .IF
   1. Select your AnB file and click on "OFMC" button.
   2. Configure OFMC: set the number of session (1,2,3...). If the number (n) is greater then one the tool will verify the protocol for 1 and n sessions in sequence.
   3. Click "OK" to verify the protocol.

ProVerif protocol verification (only for AnBx/PV files)

1. If your input file has extension .AnBx
   1. Select your AnBx file and click on "AnBxC" button. Select the output format "ProVerif (default)" and select "Launch associated validator"
   2. Optionally, click on the "gear" icon to set options for ProVerif
   3. Click "OK". The compiler will translate the file from AnBx to PV and will run ProVerif) to verify the protocol specification against the security goals.
2. If your input file has extension .PV
   1. Select your PV file and click on "ProVerif" button. Select the options ("pitype" and "solve" by default) and click "OK"

Java code generation (only for AnBx files)

You need to have configured your output directory in the anbxc.cfg file. A link is available in the root of your project.
In particular, you should check the following lines in anbxc.cfg

pathstemplates = <this is the location of the template files (.st)>
pathjavadest = <this is the location where the Java files are generated>

N.B. # on Windows use / as path separator instead of \.     Example: C:/MyWorkspace/genanbx/src/

1. Select your AnBx file and click on "AnBxC" button. Select the output format "Java"
2. Click "OK". The compiler will translate the file from AnBx to Java.
3. If you select "Launch associated validator" it will also run the generated application (using an ant build file).

Build/Run a Java Project (under Eclipse)

• Preliminaries
  1. Create a Java Project First of all, you need to create a Java project in your workspace.
     File -> New -> Project -> Java Project
     Choose the project name (and optionally the location).
     Take note of the location (e.g. C:\JavaProjects\genAnBx). Click "Finish".
     If you have already a project folder you can importing with File -> Open Projects from File System...
  2. Set the property of the Java Project Double check that you have added the AnBxJ.jar file to the libraries of your project.
     Right click on the root folder of your project, select "Properties". Then select Java Build Path -> Libraries
     If a reference to AnBxJ.jar is not present, click on "Classpath" and "Add External JARs ..." and select the location of your AnBxJ.jar file.
     You can also add a reference to Bouncy Castle cryptographic library (e.g. bcprov-jdk18on-.jar)
     The program is built automatically if the flag "Build automatically" (under the "Project" menu) is set (recommended option).
     Otherwise, select Project -> Build Project.
  3. Key store location In anbxc.cfg check that you are pointing to the right location of the keystores, containing the cryptography keys.
     The default value is
     
     # Paths
     keypath = ../../keystore/
     
     In this case you should expand the keystore file in a folder at the same level as the src folder (e.g. C:\JavaProjects\genAnBx\src\KeyStore).
  4. Where code is generated On your configuration file  anbxc.cfg check that pathjavadest
     is set to your project location source folder (e.g. pathjavadest=C:\JavaProjects\genAnBx\src)
     
     When you generate the Java code for a protocol "Prot", the files will be created under the source folder (e.g. C:\JavaProjects\genAnBx\src\Prot).
     This needs to be done only the first time, all other protocols will generate code under the protocol name folder under src.
• Running the application It can be done launching the associate ant file (build.xml). Right click and Run as -> Ant Build.
  If you select "Run associated validator" the program will run as soon as it has been generated.
  If it does not work, you need to refresh the workspace and build the project (see the console output for more details).

Refer to the online help (?) and product documentation for additional options.

Tutorial

• A tutorial on Security Programming, Protocol Verification and Code Generation

Documentation

1. AnBx IDE User Manual
2. A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols (R.Garcia, P.Modesti), Electronics, 2024, extended version
3. An IDE for the Design, Verification and Implementation of Security Protocols (R.Garcia, P.Modesti), ISSREW 2017
4. AnBx: Automatic Generation and Verification of Security Protocols Implementations (P.Modesti), FPS 2015

Questions?

• Write to