Tool Dependencies

This project currently uses the following tool versions:

• EasyCrypt: f8fab1dc5541a84b416df172522809efe8419c37
• Jasmin & ECLib: release-2025.06
• A recent C compiler (for building the test)
• Valgrind (for running the valgrind test)

Working with Docker

We provide a Docker image that includes all required dependencies. The docker can be built under Linux-x64 or MacOS-Silicon.

To build it, run:

make docker

This command creates a ready-to-use Docker image and copies the contents of this archive into the container. The corresponding Docker image at the time of submission for artifact evaluation (April 30, 2026) is also archived as ghcr.io/formosa-crypto/formosa-xmss:tches-aec.

To enter the Docker container, run:

make run-docker

This will start an interactive shell inside the container. The working directory will contain a copy of this archive.

Running the EasyCrypt security & correctness proofs

To check the proofs, run:

make -C proof

Running the test-suite / valgrind memory checker / bench

All the tests must be ran on an x64 architecture.

Running the test-suite

To run the tests, run:

make -C test/{subdir} run

where {subdir} is one of:

• sha256: runs the tests for the SHA-256 implementation.
• hash: runs the tests for THASH and other hash-based operations
• hash_address: runs the tests for operations on addresses
• wots: runs the tests for WOTS+
• treehash: runs the tests for Treehash (Jasmin implementation)
• new_treehash: runs the tests for a C implementation of Treehash matching the RFC
• xmss: runs the tests for XMSS

Running Valgrind on the implementation

You can check for memory issues with Valgrind by running:

make -C test/xmss/ check_valgrind

Running the benchmarks

You can run the benchmarks by running (all benchmarks refer to the XMSSMT-SHA2_20/2_256 parameter set):

make -C bench/ {target}.out

where {target} is one of:

• bin/bench_sha256_jasmin: Benchmarks Jasmin implementation of SHA-2 against OpenSSL, for input sizes of 32 and 64 bytes. The results are written to the files:

  • results/sha256_jasmin_ptr.txt
  • results/sha256_jasmin_32.txt
  • results/sha256_jasmin_64.txt
  • results/sha256_openssl_32.txt
  • results/sha256_openssl_64.txt

• bin/bench_wots: Benchmarks the Jasmin and C implementations of WOTS+. The results are written to the files:

  • results/expand_seed_jazz.txt
  • results/wots_checksum_jazz.txt
  • results/gen_chain_jazz.txt
  • results/wots_pkgen_jazz.txt
  • results/wots_sign_jazz.txt
  • results/wots_pk_from_sig_jazz.txt
  • results/expand_seed_c.txt
  • results/wots_checksum_c.txt
  • results/gen_chain_c.txt
  • results/wots_pkgen_c.txt
  • results/wots_sign_c.txt
  • results/wots_pk_from_sig_c.txt

• bin/bench_sha2_in_xmss_c: Benchmarks cycles consumed by SHA-256 (C implementation using OpenSSL SHA-2). Results are written to file:

  • results/bench_xmss_sha2_calls_c.csv

• bin/bench_sha2_in_xmss_jasmin: Benchmarks cycles consumed by SHA-256 (C implementation using Jasmin's SHA-2). The difference from bin/bench_sha2_in_xmss_c is that this version uses Jasmin's optimized assembly implementations. Results are written to the file:

  • results/bench_xmss_sha2_calls_jasmin.csv

• bin/bench_xmss_impl_c: Benchmarks the three XMSS-MT API operations: key generation, signature generation and verification for the C reference implementation. Results are written to the files:

  • results/bench_keygen_c.txt
  • results/bench_sign_c.txt
  • results/bench_verify_c.txt

• bin/bench_xmss_impl_jasmin: Benchmarks the three XMSS-MT API operations: key generation, signature generation and verification for the Jasmin implementation (without zeroization). Results are written to the files:

  • results/bench_keygen_jasmin.txt
  • results/bench_sign_jasmin.txt
  • results/bench_verify_jasmin.txt

• bin/bench_xmss_impl_jasmin_zero_loop: Benchmarks the three XMSS-MT API operations: key generation, signature generation and verification for the Jasmin implementation with loop-based zeroization. Results are written to the files

  • results/bench_keygen_jasmin_zero_loop.txt
  • results/bench_sign_jasmin_zero_loop.txt
  • results/bench_verify_jasmin_zero_loop.txt

• bin/bench_xmss_impl_jasmin_zero_unroll: Benchmarks the three XMSS-MT API operations: key generation, signature generation and verification for the Jasmin implementation with unrolled zeroization. Results are written to the files:

  • results/bench_keygen_jasmin_zero_unroll.txt
  • results/bench_sign_jasmin_zero_unroll.txt
  • results/bench_verify_jasmin_zero_unroll.txt

• bin/bench_treehash_c: Benchmarks the Treehash algorithm for the C reference implementation. Results are written to the file:

  • results/bench_treehash_c.txt

• bin/bench_treehash_jasmin: Benchmarks the Treehash algorithm for the Jasmin implementation. Results are written to the file:

  • results/bench_treehash_jasmin.txt

Code size

You can see the code size for each of the jasmin implementations by running:

make -C bench/ show_code_size