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, Part 6 and Part 7.

In Part 5-7 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:

• Part 1 - Java Client/Server Programming
• Part 2 - Key Generation - Secret and Authentic Channels
• Part 3 - Configuration of the cryptographic engine
• Part 4 - Implementation of a Public Key Infrastructure
• Part 5 - Security Protocols Modeling and Verification
• Part 6 - Automatic Generation of Java Implementation of Security Protocols
• Part 7 - Automatic Generation of Specifications and implementations of Attacks on Security Protocols

Tools & Libraries:

• AnBxJ Library
• AnBx Compiler and Java Code Generator
• AnBx-IDE (Eclipse Plugin)

Documentation:

• AnBx Compiler (paper)
• Eclipse Configuration
• AnBx-IDE (installation and configuration)
• AnBxJ Library
• Java Language
• Java Security

Additional readings:

• Alice and Bob, A History of The World’s Most Famous Cryptographic Couple
• OFMC Tutorial (S.Mödersheim), how to used OFMC model checker with an introduction to the AnB language
• Algebraic Properties in Alice and Bob Notation (S.Mödersheim), a paper formally describing the AnB language
• Security Protocol Specification and Verification with AnBx, a paper formally describing the AnBx language

Publications:

• Paolo Modesti
  Integrating Formal Methods for Security in Software Security Education
  Informatics in Education, Volume 19 Issue 3, 2020, pp. 425–454
• Paolo Modesti
  AnBx: Automatic Generation and Verification of Security Protocols Implementations
  International Symposium on Foundations & Practice of Security (FPS 2015), Clermont-Ferrand, France, 2015, preprint
• Rémi Garcia and Paolo Modesti
  An IDE for the Design, Verification and Implementation of Security Protocols
  IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW 2017) – AFFORD'17, Toulouse, France, 2017, preprint
• Rémi Garcia and Paolo Modesti
  Automatic Generation of Security Protocols Attacks Specifications and Implementations
  Cyber Security and Applications, Volume 1, January 2024, 1000138, 2024