Part 6 - Automatic Generation of Java Implementation of Security Protocols

We are going to automatically generate the Java implementation of security protocols using the AnBx Compiler.
For an introduction about the compiler, you can read this paper.

We provide instructions for both the command line and the Eclipse (AnBx-IDE plugin) option.
However, we strongly recommend to use Eclipse as it simplifies the configuration and utilisation of the tool.

TASK 0 - Configuration

Command Line

Download the AnBx tools and configure your environment. The source code of the application is available here.

Create a folder AnB inside the folder
Our working directory is now \AnB

In order to use the AnBx compiler you need to configure the config file. By default the file is called anbxc.cfg and should be in the same folder as the compiler executable.
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/

Eclipse plugin

Download and configure the Eclipse plugin as described here.
The same page explains also how to run the tool. Therefore, we omit here the steps for running the tools under Eclipse.
However, it important to check the configuration of your anbxc.cfg (the same applies the command line option).

TASK 1 - Code Generation

As an example we are using the Fresh_From_A.AnBx file.
We would like now generate the Java implementation for a protocol specified in AnBx.

anbxc Fresh_From_A.AnBx -out:Java

Run (Eclipse)

Click on "AnBxC" button, select the "Java" output format, press "OK".

This will generate the Java code and the config file Fresh_From_A.properties. We already meet a .properties file in Part 3. It should look like this one.
Check the parameters. In particular, be sure that you are pointing to the right location of the keystores, containing the cryptography keys.

# Paths
keypath = ../../keystore/

The agent identities are set under

# Aliases for agents A,B from the point of view of ROLE_x
ROLE_A = alice,bob
ROLE_B = alice,bob

In this case, alice will play the role "A" and bob the role "B", from the point of view of both agents.

If the protocol is also using pre-shared information (e.g. shared symmetric keys) you should check the following parameters

# Roles/Share
ROLESHARE = ROLE_A

the role that is creating the shared information

sharepath = ./

where the shared information is stored. Usually the predefined values are fine and should not changed.

Another path indicates the location of the AnBxJ library:

anbxjpath = ../../../AnBxJ

TASK 2 - Run the generated code

[cmd] Go to the folder above where the project was generated (e.g. fresh_from_a).
To compile the project run:

    javac -cp .;AnBxJ.jar fresh_from_a/*.java

To run the application from the command line:

On Windows:

java -cp .;AnBxJ.jar fresh_from_a.Fresh_From_A -r ROLE_B -verbose

java -cp .;AnBxJ.jar fresh_from_a.Fresh_From_A -r ROLE_A -verbose

On Linux or Mac:

java -cp .:AnBxJ.jar fresh_from_a.Fresh_From_A -r ROLE_B -verbose

java -cp .:AnBxJ.jar fresh_from_a.Fresh_From_A -r ROLE_A -verbose

If it does not run, try the following:

• run it again with the switch -verbose after -r ROLE_X and inspect the error messages
• check again the location of the keystores in Fresh_From_A.properties file
• check the location of the AnBxJ.jar library (in the command above it is expected to be in the folder from where the javac and java commands are run)

[ant] The compiler generates also an ant build file (build.xml). It is used to build/run the application under Eclipse.
However, it is possible to run the application using the following (indicative) syntax

    ant -buildfile build.xml <target>

where <target> is one of the targets defined in the build file.
ant is shipped with Eclipse. A stand alone version can be downloaded here.

For example

    ant -buildfile build.xml ROLE_B

    ant -buildfile build.xml ROLE_A

[Eclipse] Run (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".
  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, select "Add External JARs ..." and select the location of your AnBxJ.jar file.
     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).

TASK 3 - Inspect the generated code

Inspect the generated code, in particular the Role_X.java files.
The main program logic for each role is contained in the Role_X.java files.
Compare the implementation automatically generated with the one you built in the previous parts of the tutorial.

What are the main differences between your and this implementation?

TASK 4 - Checks on reception (Sanity checks)

anbxc Fresh_From_A.AnBx -out:Execnarr

to see in a more readable format which checks are generated by the compiler.

Compare these checks with the one you have written (if any) in the programs you have previously built by hand.
Analyse carefully the generated checks. Do you see any missing or redundant checks?
Can the code be optimised to improve the efficiency without missing any important check?

TASK 5 - Optimisation of the checks on reception

anbxc Fresh_From_A.AnBx -out:OptExecnarr

to see in a more readable format which checks are generated by the compiler.

Compare this output, with the one from the previous task.
Do you notice any difference? If yes, how do you explain such differences.

You might find more information about the optimisation procedure in this paper (Section 3.4).

TASK 6 - Running time

Compare the execution time of the two version optimised and not.
Generate the Java code. You can use the -silentcode option to suppress log messages in the generated code.

The first time use the "Java" option, the second one the "JavaNoOpt" option.
You will need to run this multiple times, as the speed of a single run can be affected by the conditions (e.g. workload) of your machine.
Under Eclispe you can use "SpeedTest" target in the ant file, or run ant from the command line. It will run the application 10 times consecutively.

TASK 7 - Generate and run other protocols

Now that you are familiar with the code generator, you can repeat the same activities with other protocols.
The more complex they are, the more likely to see differences in terms of checks, optimisation and run time speed.

You can select some complex protocols like from the protocol suite available in the AnBx distribution package available here.
Large protocols are iKP (where i={1,2,3}), SET, H530, and others.
If you would like to verify this files with OFMC be aware that the verification for 2 sessions can require very long time.

TASK 8 - Comparison of checks on reception: Manual vs Automatic generation

You can now compare the automatically generated checks with the the list of checks you have written while completing the Task 6 in Part 5.
Is there any check missing in any of the two implementations?
If yes, is this undermining the security of the protocol? Motivate your answer.