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)
• ProVerif: automatic generation of applied pi specification from AnBx/AnB model
• 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. +)
• ProVerif (+)
• Java OpenJDK and JRE are available here

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

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 following versions of the GHC: 7.8.3, 8.0.2, 8.2.2, 8.4.3, 8.6.5, 8.8.3, 8.10.7. More recent versions of GHC are untested.

• 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 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.

Running the tool (examples) (requires Java SE Runtime 11+, optional BouncyCastle library 1.72+, 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)
    • ExecNarr - Executable Narration
    • OptExecNarr - Optimized Executable Narration
    • PV: generates an untyped ProVerif model
    • PVT: generates a typed ProVerif model
• 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)
• Other options:
  • -cfg <ConfigFileName> # default: anbxc.cfg
  • -nocfgmsg # suppresses config file message display
  • -silentcode # suppresses log messages in the generated code
  • -nogoals # ignores goals in code generation in all targets except AnB
  • -noprivatekeygoals # no creation of secrecy goals for private keys used in the protocol
  • -outprotsuffix <String> # specifies a spaceless suffix for the generated protocol name and filename
    
• AnB/OFMC options:
  • -if2cif # only AnB, to be used 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)
  • -noAnBTypecheck # disables TypeChecking of AnB protocols
  • -expandbullets # expands bullet channels to AnBx channels, e.g. A*->*B: M => A->B,(A|B|B): M
    
• Code Generation & Optimization (Java/OptExecnarr) options:
  • -probenc:XX # where X=0|1 (False|True) assumes probabilistic encryption for (Asym Enc, Sym Enc) -> 11 default value automatically selected based on the target (-out:)
  • -checktype:all|opt|optfail|eq|none # find vars in all checks - default: opt all and optfail set -probenc:00, otherwise -probenc:11
  • -checkoptlevel <Int> # 0=none ... 4=full - default: 4
  • -basicopt # does not prune EQchecks which depend on previously successful EQchecks on variables applied only if optimisation on OptExecnarr is done
  • -filterfailingchecks # filter failing checks - only for (Typed)OptExecnarr, applied by default to Java
  • -maxMethodSize <Int> # max nr of actions in a Java method - default: 50
  • -maxActionsOpt <Int> # max nr of actions for Execnarr optimisation - default: 100000
  • -agent <Name> # generates only the common files and the specified agent code. <Name> is the role name
• ProVerif options:
  • -pvprobenc # assumes probabilistic encryption for both symmetric and asymmetric primitives
  • -pvreachevents # generates a reachability event at the end of each agent's process (e.g. event endX)
  • -pvtagfuntt # tags the protocol to help proving some queries where some declared functions have same argument and return type
  • -pvnomutual # does not parallelise processes by permutating free agents' names. Helps to avoid loops, and find some attacks more quickly, but may miss others (to mutual auth in particular)
  • -pvxor:none|basic|simple|ass|comm|full # declares a different xor theory in ProVerif
    • none: just declares the xor function, no equations
    • basic: basic erasure xor(xor(x,y),y) = x
    • simple: (default) basic erasure + zero
    • ass: associativity only
    • comm: commutativity only
    • full: full theory but not supported by ProVerif, at least up to version 2.04

• 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. 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

Questions?

• Write to