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 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
• AnBx-IDE available here (Eclipse plugin supporting the AnBx/AnB language and verification tools)
• New Attack trace reconstruction

Download (v. )

• For an easy setup we recommend to use the AnBx IDE
• Alternatively, download a binary package for your OS:
  • Windows (x64)
  • Linux
  • Mac

Tutorial

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

Components

• AnBx Compiler and Code generator (source code + win executable)
• AnBxJ - Java Security Library: JAR file | Documentation
• AnBx-IDE (Eclipse plug-in 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)
    • AnBIF - AVISPA IF (OFMC)
    • Java - Generates the Java source code of the application (details here)
    • JavaDocker: Generate Java code for distributed Docker container
    • ExecNarr - Executable Narration
    • OptExecNarr - Optimized Executable Narration
    • PV: generates an untyped ProVerif model
    • PVT: generates a typed ProVerif model
    • AnBxLatex|AnBLatex: Generate AnBx|AnB sequence diagram Latex code
• 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
• Main options:
  • -cfg <ConfigFileName> # default: anbxc.cfg
  • -silent # Suppress display of generated files and config file messages
  • -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
  • -passiveintruder # Introduce a passive intruder in the code generation (similar to -out:AnBxIntr)
    
• AnB/OFMC options:
  • -if2cif # only AnB, to be used in combination with OFMC --IF2CIF
  • -ifsessions # Specify the sessions for the generated IF code (AnBIF only)
  • -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
  • -ofmctrace # Specify the OFMC attack trace file for reconstruction to an AnBx protocol
    
• Code Generation & Optimization (Java/OptExecnarr) options:
  • -probenc:XX # where X=0|1 (False|True) Assume probabilistic encryption for (Asym Enc, Sym Enc) -> 1 - 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 # Do not prune EQchecks that 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> # Maximum number of actions in a Java method (default: 50)
  • -maxActionsOpt <Int> # Maximum number of actions for Execnarr optimisation (default: 100000)
  • -agent <String> # Generate only the common files and the specified agent code. <String> is the agent's name
  • -jfr # Enable Java Flight Recording
  • -jfrlabel <String> # Specify a label that can be added to the filename saved in JFR
  • -jdockerpcap # Enable packet capture (PCAP) - Only if the output type is JavaDocker
  • -jdockercpuquota <Int> # CPU quota for Docker containers. Use units like '200000' for 200,000 CPU shares. Set to 0 for no CPU limit
  • -jdockermemlimit <Int><unit> # Memory limit for Docker containers. Unit: b|k|m|g for bytes|kb|Mb|Gb. Set to 0 for no memory limit
  • -jsessions <Int> # Specify the number of runs of the protocol in Java
  • -jabortonfail # Specify if an agent should abort the run of the protocol in Java if an error occurs
• 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)
  • -pvpreciseactions # set preciseActions = true. in the generated co
  • -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 it is not supported by ProVerif, at least up to version 2.05
• Cryptographic configuration options:
  • -cipherScheme <String> # Specify symmetric encryption cipher scheme
  • -keySize <Int> # Specify the key size for the symmetric encryption cipher scheme
  • -keyGenerationScheme <String> # Specify the key generation scheme
  • -keyGenerationSchemePBE <String> # Specify the PBE key generation scheme
  • -keyGenerationSize <Int> # Specify the size of the generated keys
  • -keyPairGenerationScheme <String> # Specify the key pair generation scheme
  • -keyPairGenerationSize <Int> # Specify the key pair generation size
  • -secureRandomAlgorithm <String> # Specify the secure random algorithm
  • -hMacAlgorithm <String> # Specify the HMAC algorithm
  • -messageDigestAlgorithm <String> # Specify the message digest algorithm
  • -keyAgreementAlgorithm <String> # Specify the key agreement algorithm
  • -keyAgreementKeyPairGenerationScheme <String> # Specify the key pair generation scheme for key agreement algorithm
  • -dhRndExpSize <Int> # Specify the Diffie-Hellman random exponent size
  • -ecGenParameterSpec <String> # Specify the elliptic curve used in ECDH key agreement
  • -asymcipherSchemeBlock <String> # Specify the asymmetric cipher scheme block (experimental)
  • -sslContext <String> # Specify the SSL context algorithm (e.g. TLSv1.3)
  • -securityProvider <String> # Specify the security provider (overrides java.security settings)

• 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

We strongly recommend to install the Glasgow Haskell Compiler (GHC) and cabal using ghcup.
We have tested the build with the several versions of the GHC up to 9.4.8, which is the recommended version. More recent versions of GHC are untested.

• Download the source code, then run (within the directory where the .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 .cabal file.

Papers and Documentation

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

Questions?

• Write to