Senior Lecturer in Cybersecurity

Paolo Modesti

AnBx Compiler and Java Code Generator

Security Protocols Specification, Verification and Implementation - Alice and Bob to Java Compiler

Lead author: Paolo Modesti - Contributor: Rémi Garcia


Download (v. )



Running the tool (examples) (requires Java SE Runtime 11+, optional BouncyCastle library +, for more ciphers and algorithms)

Java Code Generation

Building the tool

We strongly recommend to install the Glasgow Haskell Compiler (GHC) and cabal using ghcup.
We have tested the build with the several versions of the GHC up to 9.4.8, which is the recommended version. More recent versions of GHC are untested.

In order to build the application, additional Haskell packages are required.
Running cabal install --only-dependencies should download and install these dependencies for you.

If an error persists, the compiler should tell you which packages are missing.
At least the following packages must be installed before being able to build the application.

cabal install HStringTemplate
cabal install filepath
cabal install ConfigFile
cabal install MissingH
cabal install utf8-string

Then run again:

cabal configure
cabal build

If you struggle to identify missing dependencies look at the build-depends: section in the .cabal file.

Papers and Documentation

  1. Automatic Generation of Security Protocols Attacks Specifications and Implementations (R.Garcia, P.Modesti), CSA, 2024
  2. Integrating Formal Methods for Security in Software Security Education (P.Modesti), Informatics in Education, 2020
  3. An IDE for the Design, Verification and Implementation of Security Protocols (R.Garcia, P.Modesti), ISSREW2017
  4. Security Protocol Specification and Verification with AnBx (M.Bugliesi, S.Calzavara, S.Mödersheim, P.Modesti), JISA 2016
  5. AnBx: Automatic Generation and Verification of Security Protocols Implementations (P.Modesti), FPS 2015
  6. Efficient Java Code Generation of Security Protocols specified in AnB/AnBx (P.Modesti), Technical Report 2014
  7. Efficient Java Code Generation of Security Protocols specified in AnB/AnBx (P.Modesti), STM 2014 (Short Paper)
  8. AnBx - Security Protocols Design and Verification (M.Bugliesi, P.Modesti), ARSPA-WITS 2010