Senior Lecturer in Cybersecurity
, UK

Paolo Modesti

AnBx Compiler and Java Code Generator

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


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 (requires the Glasgow Haskell Compiler)

We highly recommend to install a Haskell package that includes a number of core and widely used packages.
We have tested the build with the many versions of the GHC, including 8.10.7 and 9.2.7. 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 AnBx2.cabal file.

Papers and Documentation

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