This is the Eclipse Update Site for the AnBx-IDE

Installation
The simplest way is to install the plugin from the Eclipse Marketplace using this button Drag to your running Eclipse* workspace. *Requires Eclipse Marketplace Client
Drag and drop the button on your Eclipse Workspace.

Alternatevely, you can install it 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 http://www.dais.unive.it/~modesti/anbx/ for the update site.

Download and installation of tools

Along with the Eclipse Plug-in, the AnBx-IDE requires to download and configure the following software:

Windows: For convenience we provide a zip file with the executables for Windows, AnBxJ library and Java templates.
Other operating systems: Check if the distribution package contains an executable for your operating system, otherwise you will need to build your own executables.
For the procedure to build each tool refer to documenation of the package.

Optional components

Configuration of the plugin

To configure the plugin, in Eclipse select "AnBx Tools -> Configuration", and set the paths to the execuables of these tools and to the config file anbxc.cfg.
If you have downloaded the zip file with the executable and auxilliary files, in order to work with this plugin, 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

The working directories are usually set to the one where the executable are located.

Create a 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

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. Use Grep Console to display the output in colors.

OFMC protocol verification (only for AnBx/AnB files)

  1. If you input file has extension .AnBx
    1. (Only the first time) 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 session in sequence.
    2. Select your AnBx file and click on the "AnBxC" button. Select the output format "AnB (default)" and select "Launch associated validator"
    3. 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 you input file has extension .AnB
    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 you 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. 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 you input file has extension .PV
    1. Select your PV file and click on "ProVerif" button. Select the option ("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 at 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).

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

Enjoy!

Rémi Garcia and Paolo Modesti

Questions? write to

Documentation

  1. An IDE for the Design, Verification and Implementation of Security Protocols (R.Garcia, P.Modesti), ISSREW2017