Security Tutorial (Java/AnBx)

Security Programming, Protocol Verification and Code Generation
Paolo Modesti -

Welcome to this tutorial on Security Programming, Protocol Verification and Code Generation!

You will learn how to implement security protocols using Java and the AnBxJ library.
The AnBxJ library is a Java library, based on the Java Cryptography Architecture (JCA),
which allows to use many cryptographic and communication functions in a simple and effective way.

Moreover, you will run experiments to verify security properties of these protocols.
You will also learn how to automatically generated Java implementation for these protocols.

You will use the command line interface to configure the environment, compile and run Java programs. You may use any editor to edit the source files.

If you are only interested in AnB/AnBx you can directly go to Part 5 and Part 6.

In Part 5 and 6 we are going to use the Eclipse IDE with the AnBx-IDE plugin. Therefore, feel free to use Eclipse for all activities. The required configuration for Eclipse is available here.

Some tasks are marked as "optional"; if you do not have much time you can skip them.

This tutorial comprises the following parts:

Tools & Libraries:

Documentation:

Additional readings:

Publications: