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 - Documentation:
- AnBx Compiler (tool)
- AnBx Compiler (paper)
- Eclipse Configuration
- AnBx IDE (installation and configuration)
- AnBx IDE Manual
- 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
A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols
Electronics, Volume 13, no. 23, 4660, 2024, extended version - 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