# AnBx Compiler and Code Generator

**Lead author**: Paolo Modesti  
**Contributor**: Rémi Garcia

This document contains a summary of the instructions required for building and running the AnBx Compiler and Code Generator. Full details are available at [https://paolo.science/anbx/](https://paolo.science/anbx/)

An Eclipse-based IDE for AnBx is available at [https://paolo.science/anbx/ide/](https://paolo.science/anbx/ide/)  
Using this IDE is the simplest way to configure and run the tool.

The software is distributed under the **GNU GPLv3 licence**.

For any questions/comments, or to be notified of new releases, write to: p.modesti (at) tees.ac.uk

**Have fun!**

## Distribution Package Outline

**Contents - Sources and binaries:**

- `\AnBx2` → AnBx compiler src, binary file, config-file, templates
- `\AnBxJ` → AnBxJ security library and src + Bouncy Castle .jar
- `\casestudies` → AnB and AnBx protocols
- `\casestudies.DYStar` → AnB and AnBx protocols for DYStar code generation
- `\dystar_lib` → DYStar libraries
- `\ext-tools` → External tools (OFMC, ProVerif binaries)
- `\genAnBx\src` → Generated Java source code
- `\genAnBx\keystore` → Keystores (cryptographic keys)

## Basic Usage

To generate the JAVA implementation:

anbxc <filename> -out:Java

To generate the typed ProVerif specification
anbxc <filename> -out:PVT

for the untyped ProVerif use
anbxc <filename> -out:PV

N.B if the config file anbxc.cfg is in the same folder of executable,
there is no need to use the option -cfg: <configfilename>

## Requirements

**Building the tools**: GHC 9.6.7+ (See: [https://www.haskell.org/](https://www.haskell.org/))  
**Running the generated Java code**: JDK is required to compile Java files; the recommended Java version is 21.

The optional Bouncy Castle Library is required to support more ciphers and algorithms than the standard JDK supported ones.

## Permissions on Linux and Mac

On Mac and Linux you will likely need to set execution permissions to the binary files. 
The simplest way is to run the bash script `setexecpermissions.sh` available in the distribution package. 
Depending on the configuration you may need to run the script with sudo. The script automates the process described below:

To set the executable permissions, you can run the command
chmod u+x <filename>
or use the operating system’s GUI for setting permissions.

On Mac, you may also need to authorise the execution of the binary files in System Preferences -> Security and Privacy, go to General tab and click Allow.
From the command line, this step can be done from the command line with this command 
xattr -dr com.apple.quarantine <filename>
where <filename> indicates the file of interest.

## Running ProVerif on Linux 

If trying to run Proverif under Linux and you experience an error similar to this one:

proverif: /lib/x86_64-linux-gnu/libm.so.6: version `GLIBC_2.38' not found (required by ProVerif)

you may need to install the missing library. Run this command: sudo apt install libc6

The following document may be useful:
https://www.cyberithub.com/how-do-i-install-the-linux-library-libc-so-6-in-5-easy-steps/

## Java (Docker)

Executing generated Java code in a Docker distributed system requires Docker to be installed, and Docker Engine running.
Installing Docker Desktop is the simplest option:
https://docs.docker.com/get-docker/

On Linux systems, if "docker compose" command is not available, you may need to install the "docker-compose-plugin"
https://docs.docker.com/compose/install/linux/"

## Upgrade from a previous version

It is recommended to rename the folder containing the old version and extract the new files on the same folder as the old one.
However, if the config file (anbxc.cfg) has been customised, some care is required.
It advisable to make a backup of this file and restore it after updating all other files.
Make sure all files are up to date, including the library (AnBxJ.jar) and the template files (*.st).
Finally, if you use JavaDocker, it is advisable to rebuild the images, as the Dockerfile(s) may have been updated.
Run the following commands to delete the current images. They will be rebuild at the first usage.

docker rmi anbx_dy:1.0.0
docker rmi anbx:1.0.0

Specific version upgrade information:

- From version 2025.09, fields in the config file (anbxc.cfg) are organised in sections.
To migrate to the new standard, simply add the following line on top of your existing config file:
[Default]

From this version, Config file can be automatically updated when a new version is released.

## Notes 
--------
In Java, AnB bullet channels (e.g. *->*) are implemented using TLSv1.2 or TLSv1.3

In order to enable the Java implementation of AnB bullet channel *-> and ->*
it is necessary to remove "anon, NULL" from 
the jdk.tls.disabledAlgorithms entry in the java.security file. e.g.

jdk.tls.disabledAlgorithms=SSLv3, TLSv1, TLSv1.1, RC4, DES, MD5withRSA, \
    DH keySize < 1024, EC keySize < 224, 3DES_EDE_CBC, anon, NULL, \
    include jdk.disabled.namedCurves

See: https://bugs.java.com/bugdatabase/view_bug.do?bug_id=JDK-8211883

For more information on Java Cryptography configuration, visit: https://www.java.com/en/configure_crypto.html

------------------------------------------------------------------------------------------------------------
## Provable prototyping for provable prototypes: translating Alice & Bob to F*

### Preparation

1. You can compile the AnBx Compiler sources with
  `cabal build`
  The AnBx.cabal file orchestrates the compilation, and the binary is exported in dist-newstyle folder.
  With the current configuration given by anbxc.cfg, the generated code will be found in `genAnBx/src/DYStar`.

2. Install the F\* distribution to run the case studies. Run
   `opam install fstar.2025.09.04`
   The Z3 executable it uses is present in the current directory, make sure it is in your PATH.
   If you want finer control over your F\*/Z3 setup, refer to the installation instructions here:
   https://github.com/FStarLang/FStar/blob/master/INSTALL.md

3. Initialise the environment variables for DY\*:
   `export FSTAR_HOME=~/.opam/default`
   `export DY_HOME=./dystar_lib`

4. Download Z3 from https://github.com/Z3Prover/z3/releases 
   add it to the system PATH.


### Verify and prepare the DY* framework

 - To verify the core symbolic model, go into the `dystar_lib` folder and
   just run `make`. This will invoke F\* for all modules in the core model, F\* verifies (i.e., typechecks)
   these files. For the concrete counterpart of DY\*, run `make -f Makefile.concrete`.
   The same can be done for the Comparse component of DY\*, in the `dystar_lib/comparse` folder.
 
 - Under `dystar_lib/concrete/hacl-star-snapshot` there are HACL\* files for the cryptographic primitives used for
   concrete execution. Running make in this folder compiles the HACL\* files for later usage.


### Verifying and executing test cases

These instructions assume that you followed the steps in the
preparation subsection and have an open shell inside the docker
container.

1. Verify (typecheck) the core DY\* as described above.
   To verify one of the protocol implementations, `cd` into the
   respective directory (e.g., `cd NSL`).  Inside the protocol
   directory, run `make`, which will verify (typecheck) all modules of
   the protocol implementation.

2. `cd` into the protocol directory and run `make test`.
   This compiles the F\* code to OCaml executing symbolic operations and then
   compiles the OCaml code into an executable file (namely `test.exe`).
   To export the F\* to concrete code that uses HACL\*, use `make test -f Makefile.concrete` instead.

3. `cd` into the subfolder `ocaml-symbolic` or `ocaml-concrete` in the protocol directory

4. Run `./test.exe` to execute the test cases. This will print some
   intermediate information and at least one execution trace.

---
AnBx Compiler and Code Generator - Version 2025.11
Support website: https://paolo.science/anbx/
Usage:
anbxc <AnBxFileName> [options]

anbxc -v # Print the product name and version
anbxc -help | ? # Print the help screen with the complete list of options

------ Options: ------
-impl:AANB|CIF|CIF2|CIF3 # implementation of AnBx channels

	CIF: Default implementation  (freshness: Sequence Numbers, encryption: PKI)
	CIF2: Alternative implementation (freshness: Challenge/Response, encryption: PKI)
	CIF3: Another alternative implementation (freshness: DH, encryption: PKI)
	AANB: Annotated AnB implementation (freshness: Sequence Numbers, encryption: PKI)

-debug:None|AnBx|AnB|AnB2AnBx|AnBEqTheory|Java|AnBIntrGoal|SpyerPN|Defs|Execnarr|NExecnarr|OptExecnarr|KnowExecnarr|PV|PVT|PVTAnB|PVTJava|PVTCBAB|DYStar|VDM
-out:AnB|Java|JavaNoOpt|JavaDocker|SpyerPN|Execnarr|OptExecnarr|TypedOptExecnarr|TypedOptExecnarrDocker|KnowExecnarr|PV|PVT|PVTAnB|PVTJava|PVTCBAB|DYStar|VDM
        |AnBxIntr|AnBIntr|AnBEqTheory|AnBIF|AnBStats|AnBStatsCSV|AnBx

	AnB: Generate AnB code
	Java: Generate Java code
	JavaNoOpt: Generate Java code without cryptographic optimisation
	JavaDocker: Generate Java code for distributed Docker containers
	SpyerPN: Generate Spyer code (legacy)
	Execnarr|OptExecnarr|TypedOptExecnarr|TypedOptExecnarrDocker: Generate intermediate formats for code generation
	KnowExecnarr: Generate agents' knowledge at the end of the protocol run
	PV: Generate an untyped ProVerif model
	PVT: Generate a typed ProVerif model
	PVTAnB: Generate a typed ProVerif model mapping types as in AnB
	PVTJava: Generate a typed ProVerif model mapping types as in Java
	PVTCBAB: Generate a typed ProVerif model mapping "ByteArray" types to "bitstring"
	DYStar: Generate DY* code
	VDM: Generate VDM code (experimental)
	AnBxIntr|AnBIntr: Generate AnBx|AnB code with explicit intruder/MITM (default: intr)
	   The name can be specified with -mitm, e.g., -mitm Intruder
	   Optionally, use -pubmitmknow to publish the initial knowledge of the MITM agent
	AnBEqTheory: Generate an OFMC theory file (.thy) if the protocol declares equational theories
	AnBIF: Generate IF code (experimental)
	AnBStats: Generate statistics about the AnB protocol
	AnBStatsCSV: Generate statistics about the AnB protocol in CSV format
	AnBxLatex|AnBLatex: Generate AnBx|AnB sequence diagram Latex code

-cfg <ConfigFileName> # Specify the config file - default: anbxc.cfg
-printdefaultconfig # Print default config file
-silent # Suppress display of generated files and config file messages
-nocfgmsg # Suppress display of config file messages only
-silentcode # Suppress log messages in the generated code
-omitverdatetime # Omit displaying version and date time in generated code
-nogoals # Ignore goals in code generation in all targets except AnB
-noprivatekeygoals # Skip creation of secrecy goals for private keys used in the protocol
-outprotsuffix <String> # Specify a suffix for the generated protocol name and filename (without spaces)
-ofmctrace # Specify the OFMC attack trace file for reconstruction to an AnBx protocol
-passiveintruder # Introduce a passive intruder in the code generation (similar to -out:AnBxIntr)
-replicate <Int> # Replicate the actions n times and save the protocol as <filename>_xn.AnBx (n > 1, AnBx target only)
-objcheck # Allow the passive intruder to check reconstructed serialised messages stored as .ser files
            Expected FileName: $prot$_STEP_#.ser

------ OFMC/AnB options: ------
-if2cif # AnB only, to be used in combination with OFMC switch --IF2CIF
-ifsessions <Int> # Specify the number of sessions for the generated IF code (n > 0, AnBIF only) (default: 2)
-noAnBTypeCheck # Disable type checking of AnB protocols
-noAnBExecCheck # Disable executability checking of AnB protocols
-noAnBKnowCheck # Disable checking that all agents have a declared initial knowledge in AnB protocols
-expandbullets # Expand bullet channels to AnBx channels, e.g., A*->*B: M => A->B,(A|B|B): M
-anbxusetags # Use tags when compiling AnBx channels to AnB
-guessprivatefunctions # Guess private functions/mappings in AnB protocols (experimental)
-noshareguess # Disable automatic guessing of pre-shared information from knowledge in AnB protocols
                Note: Private functions can be declared as Function [T1,...,Tn ->* T] f

------ Single/Group goal generation options: ------
-singlegoals # Generate AnB/ProVerif files with a single goal each
-goalindex <Int> # Generate an AnB/ProVerif file with the <Int>-th goal
-groupgoals # Generate AnB/ProVerif files grouping goals of the same type (Auth,WAuth,ChGoal,Conf)

------ Code Generation & Optimisation (Java|ProVerif|(Typed)OptExecnarr) options: ------
-probenc:XX # where X=0|1 (False|True)
              Assume 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 # 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
-effstepvarmap # Sort executable narration actions by effective step number during the optimisation process
-jsessions <Int> # Number of protocol executions to perform in Java
-jabortonfail # Abort the protocol run if an error occurs in a Java agent
-jexectime # Display execution time for cryptographic operations in Java (default: off)
-noExecnarrTypeCheck # Disable type checking of Execnarr actions and declarations
-allpublickeysknown # All known public keys are added to every agent's knowledge

------ Docker & JFR (Java|JavaDocker) options: ------
-jfr # Enable Java Flight Recording
-jfrlabel <String> # Specify a label that can be added to the filename saved in JFR
-jfrsettings default|profile|<FilePath> # Specify the JFR settings file, default|profile|<FilePath>
-jdockerpcap # Enable packet capture (PCAP) - JavaDocker output only
-jdockercpuquota <Int> # Maximum CPU time container can use per period in microseconds [1000-1000000]. 0 means use Docker default
-jdockercpuperiod <Int> # CPU allocation period length in microseconds [1000-1000000]. 0 means use Docker default
-jdockercpumhzhost <Double> # Host CPU frequency in MHz; used only in combination with -jdockercpumhzcontainer
-jdockercpumhzcontainer <Double> # Container CPU frequency in MHz; used only in combination with -jdockercpumhzhost
-jdockermemlimit <Int><unit> # Set memory limit for Docker containers. Units: b|k|m|g for bytes|kb|Mb|Gb. 0 means use Docker default

------ ProVerif options: ------
-pvprobenc # Assume probabilistic encryption for both symmetric and asymmetric primitives
-pvreachevents # Generate a reachability event at the end of each agent's process (e.g., event endX)
-pvpreciseactions # Set preciseActions = true in the generated code, to increase the precision of the solving procedure
-pvmovenew # Set movenew = true in the generated code, to increase the precision of the solving procedure
-pvmovenewup # Move certain new statements upwards to reduce analysis cost of large models
-pvverbosegoalreachable # Set verboseGoalReachable = true in the generated code. Displays each derivable clause that satisfies the query
-pvverbosestatistics # Set verboseStatistics = true in the generated code. Displays more statistics during the verification process
-pvtagfuntt # Tag the protocol to help prove some queries
              particularly when declared functions share the same argument and return type
-pvnomutual # Do not parallelise the main process by permutating free agents' names. This helps avoid loops
              and may find some attacks more quickly, but could miss others (e.g., mutual authentication)
-pvxor:none|basic|simple|ass|comm|full # Declare an XOR theory for ProVerif
	none: Declare only the XOR function, no equations
	basic: Basic erasure, i.e., xor(xor(x, y), y) = x
	simple: (default) basic erasure + identity for zero
	ass: Associativity only
	comm: Commutativity only
	full: Full theory (not supported by ProVerif as of version 2.05)

Examples:
anbxc <AnBxFileName> -out:PVT -nogoals -pvreachevents # Verify reachability events only; all should
                                                        be "false" or at least "cannot be proved"
anbxc <AnBxFileName> -out:PVT -pvnomutual # Help to avoid loops, and find some attacks more quickly,
                                            but may miss others (mutual auth goals in particular)
anbxc <AnBxFileName> -out:PVT # Standard verification of the typed model

------ VDM (experimental) options: ------
Usage: anbxc <VDMFolder> options

-vdmtest:SG|WF # Generate VDM test file; the main argument <VDMFolder> should be a folder with vdmsl files
                 Test Types: SG (Security Goals), WF (Well-Formedness)
-vdmtestmodulename <ModuleName> # Specify the module name for the test file, otherwise these defaults are used
                                  SG: AnB_trace_satisfy_goals, WF: AnB_trace_wf

------ Cryptographic configuration options: ------
-cipherScheme <String> # Specify symmetric encryption cipher scheme for static (pre-shared) keys
-keySize <Int> # Specify the key size (in bits) for the symmetric encryption cipher scheme for static (pre-shared) keys
-keyGenerationScheme <String> # Specify the symmetric cipher algorithm for ephemeral key generation
-keyGenerationSchemePBE <String> # Specify the PBE key generation scheme
-keyGenerationSize <Int> # Specify the key size (in bits) for dynamically generated symmetric 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
-hMacKeySize <Int> # Specify the key size for the HMAC algorithm
-messageDigestAlgorithm <String> # Specify the message digest algorithm
-messageDigestSignatureAlgorithm <String> # Specify the message digest for signature algorithm
                                            For key pair generation scheme only
-keyAgreementAlgorithm <String> # Specify the key agreement algorithm
-keyAgreementKeyPairGenerationScheme <String> # Specify the key pair generation scheme for key agreement algorithm
-dhModulusSize <Int> # Specify the Diffie-Hellman modulus 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)
-keyTypeToCipher <String> # Add or override entries in the key type to cipher transformation mapping,
                            format: KeyType->Cipher[,KeyType,Cipher...] (no spaces)
-keyTypeToSignature <String> # Add or override entries in the key type to signature algorithm mapping,
                               format: KeyType->Signature[,KeyType,Signature...] (no spaces)
----------------------------------------------------
 
Credit: almost all of the following examples are adapted from the AnB models distributed with OFMC by Sebastian Mödersheim 
        available at https://www2.imm.dtu.dk/~samo/ under BSD licence 
 
Amended_NSCK.AnBx
AndrewSecureRPC.AnBx
AndrewSecureRPCSecrecy.AnBx
Basic_Kerberos.AnBx
Bilateral_Key_Exchange.AnBx
Carlsen.AnBx
DenningSacco.AnBx
DenningSaccoCorr.AnBx
EPMO.AnBx
IKEv2DS.AnBx
ISO4pass.AnBx
ISO5pass.AnBx
ISOCCFOnePassUnilateralAuthProt.AnBx
ISOCCFThreePassMutual.AnBx
ISOCCFTwoPassMutualAuthProtCorr.AnBx
ISOCCFTwoPassUnilateralAuthProt.AnBx
ISOpubKeyOnePassUnilateralAuthProt.AnBx
ISOpubKeyTwoPassMutualAuthProt.AnBx
ISOpubKeyTwoPassMutualAuthProtCorr.AnBx
ISOpubKeyTwoPassUnilateralAuthProt.AnBx
ISOsymKeyOnePassUnilateralAuthProt.AnBx
ISOsymKeyThreePassMutual.AnBx
ISOsymKeyTwoPassMutualAuthProtCorr.AnBx
ISOsymKeyTwoPassUnilateralAuthProt.AnBx
Kerberos_PKINIT.AnBx
KeyEx1.AnBx
KeyEx2.AnBx
KeyEx3.AnBx
KeyEx3b.AnBx
KeyEx4.AnBx
KeyEx4b.AnBx
KeyEx5.AnBx
KeyEx5b.AnBx
KeyEx5c.AnBx
KeyEx6.AnBx
NonReversible.AnBx
NSCK.AnBx
NSL.AnBx
NSL_KeyServer.AnBx
NSPK.AnBx
NSPK_KeyServer.AnBx
Otway_Rees.AnBx
SSO.AnBx
TLS.AnBx
TLS_noClientAuth.AnBx
TLS_pw.AnBx
WL92.AnBx
WMF.AnBx
WooLam.AnBx
WooLam1.AnBx
WooLam1Test.AnBx
WooLam2.AnBx
WooLam3.AnBx
WooLam4.AnBx
WooLamF.AnBx
WooLamMutual.AnBx
Yahalom.AnBx
-----------------------------------------------------------------------------------------------------------------------

Bouncy Castle Java Library (optional)
-------------------------------------

The following version is included in this AnBx distribution package: bcprov-jdk18on-1.82.jar 
Newer versions can be downloaded from: https://www.bouncycastle.org/latest_releases.html 
Installation: https://www.bouncycastle.org/wiki/display/JA1/Provider+Installation
Bouncy Castle is released under MIT License: http://opensource.org/licenses/MIT
Copyright (c) 2000 - 2025 The Legion of the Bouncy Castle Inc. (https://www.bouncycastle.org)

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 

