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)
- ProVerif: automatic generation of typed and untyped 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, VDM-SL
- New AnBx-IDE available here (Eclipse plugin supporting the AnBx/AnB language and verification tools)
Download (v. )
- For an easy setup we recommend to use the AnBx IDE
- Alternatively, download a binary package for your OS:
Tutorial
Components
- 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
Running the tool (examples) (requires Java SE Runtime 11+, optional BouncyCastle library +, 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
- Output -out:
- 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)
- 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
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.
- Download the
source code, then run
(from the directory where the AnBx3.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.
Papers and Documentation
- Integrating Formal Methods for Security in Software Security Education (P.Modesti), Informatics in Education, 2020
- 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