AnBx Compiler and Java Code Generator

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

• AnBx to AnB compiler for verification (requires the OFMC model-checker)
• Java code generator from AnBx or AnB specification
• Java library for security (AnBxJ)
• Output formats: AnB, Spyer, Executable Narrations, Optimized Executable Narrations, Applied-Pi [ProVerif], Java
• New AnBx-IDE available here (Eclipse plugin supporting the AnBx/AnB language and verification tools)

Download (v. ) - N.B. For an easy setup we recommend to use the AnBx IDE.

• AnBx Compiler and Code generator (source code + win executable)
• AnBxJ - Java Security Library: JAR file | Documentation
• AnBx-IDE (Eclipse-based for AnBx)
• OFMC model checker: source code, executables and docs available here (v. 2020+)
• ProVerif (2.02+)
• Java OpenJDK and JRE are available here

Building the tool (requires the Glasgow Haskell Compiler version 7.8.3+)

We highly recommend to install the Haskell platform as it includes a number of core and widely used packages.
We have tested the build with the following versions of the GHC: 7.8.3, 8.0.2, 8.2.2, 8.4.3, 8.6.5, 8.8.3. More recent versions of GHC are untested.
"Prior" releases of the Haskell platform can be downloaded from here.

• Download the source code, then run (from the directory where the AnBx2.cabal file is stored):
   
  • cabal update
  • cabal install --only-dependencies
  • cabal configure
  • cabal build

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 persist, 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.

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

• anbxc <AnBxFileName> -out:AnB generates the AnB file (with the default implementation)
  • Output -out:
    • AnB - Alice and Bob notation (OFMC)
    • Java - Generates the Java source code of the application (details here)
    • PV - Generated applied-pi specification for ProVerif
    • ExecNarr - Executable Narration
    • OptExecNarr - Optimized Executable Narration
• anbxc <AnBxFileName> -impl:CIF -out:AnB generates the AnB file with CIF implementation
  • Implementations -impl:
    • CIF is a standard implementation (freshness: Sequence Numbers, encryption: PKI) (default)
    • CIF2 is an alternative implementation (freshness: Challenge/Response, encryption: PKI)
    • CIF3 is an alternative (freshness: DH, encryption: PKI)
    • AANB (Annotated AnB) is intended for further translation in cryptIF
      anbxc <AnBxFileName> -impl:AANB -out:ANB | ofmc --ot IF --if2cif
• anbxc <AnBxFileName> -impl:CIF -out:ANB | ofmc --ot IF     # generates AnB and AVISPA IF (requires OFMC)
  
• additional switches
  • -if2cif # only AnB, to be use in combination with OFMC --if2cif
  • -singlegoals # generates AnB files with a single goal each
  • -goalindex <INT> # generates an AnB file with the INT-th goal
  • -groupgoals # generates AnB files grouping goals of the same type (Auth,WAuth,ChGoal,Conf)
    
• Code Generation & Optimization (Java/OptExecnarr)
  • -checktype:all|opt|optfail|eq|none # find vars in all checks - default: opt
  • -checkoptlevel <Int> # 0=none ... 4=full - default: 4
  • -basicopt do not prune eqchecks which are dependant from previous successfull eqchecks on variables applied only if optimization on OptExecnarr is done
  • -maxMethodSize <Int> # max nr of actions in a Java method - default: 50
  • -maxActionsOpt <Int> # max nr of actions for execnarr optimization - default: 100000
  • -agent <Name> # generate only the common files and the specified agent code. <Name> is the role name

• The following files are needed:
  • anbxc.cfg a configuration file, recommended to be in the same folder as the anbxc executable, must be edited to set source and destination folders
  • java templates (including a build.xml template useful to run the application within the Eclipse IDE or from the command line)
  • AnBxJ.jar, run-time support for the generated application
  • sample self-signed public/private keys (Alice,Bob,Charlie,Dave,Eve,Frank,...) to be used with the demo applications
    The keys are generated with the Java keytool.
• then run
  • anbxc <AnBxFileName> -out:Java

Tutorial

• A tutorial on Security Programming, Protocol Verification and Code Generation

Papers and Documentation

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

Questions?

• Write to