AnBx Compiler and Java Code Generator
Security Protocols Specification, Verification and Implementation - Alice and Bob to Java Compiler
Features- 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
- 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)
- 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
- Implementations -impl:
- 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
Papers and Documentation
- An IDE for the Design, Verification and Implementation of Security Protocols (R.Garcia, P.Modesti), ISSREW2017
- Security Protocol Specification and Verification with AnBx (M.Bugliesi, S.Calzavara, S.Mödersheim, P.Modesti), JISA 2016
- AnBx: Automatic Generation and Verification of Security Protocols Implementations (P.Modesti), FPS 2015
- Efficient Java Code Generation of Security Protocols specified in AnB/AnBx (P.Modesti), Technical Report 2014
- Efficient Java Code Generation of Security Protocols specified in AnB/AnBx (P.Modesti), STM 2014 (Short Paper)
- AnBx - Security Protocols Design and Verification (M.Bugliesi, P.Modesti), ARSPA-WITS 2010
Questions?
- Write to