Hax and F* Verification

We use Hax to extract our Rust implementation into F*, a proof-oriented programming language. The extracted code is then verified against security axioms in an abstract cryptography module. This document explains the extraction pipeline, the AbstractCrypto module, and how to run verification.

What is Hax?

Hax is a tool that extracts Rust code into verification-friendly formats: F*, Coq, or Lean. Unlike ProVerif—which verifies hand-written models—Hax verifies the actual implementation code. The extraction process:

1. Parses and type-checks the Rust code
2. Translates it into the target proof language (F* in our case)
3. Replaces cryptographic primitives with abstract stubs when crypto-backend is disabled

F* is a functional programming language with a powerful type system. Types can encode invariants and security properties; the F* type checker verifies that the code satisfies these properties.

Extraction Pipeline

Prerequisites

• OPAM and OCaml: sudo apt install opam, then opam init and opam switch create 5.1.1
• F*: opam install fstar
• Hax engine: Clone from hacspec/hax, run ./setup.sh
• Cargo, Node.js, jq: For the build toolchain

Extraction Command

Important: Extraction must be done without the crypto-backend feature so that crypto calls become abstract stubs:

cd signal-protocol-core
cargo hax -C --no-default-features \; into fstar --z3rlimit 40

This generates F* files in proofs/fstar/extraction/.

Makefile Workflow

cd signal-protocol-core/proofs/fstar/extraction

make extract   # Extract only (no verification)
make verify    # Verify all F* modules
make          # Extract and verify
make verify-lite   # Verify without Double Ratchet (faster, less resource-heavy)

Double Ratchet verification is resource-intensive (--z3rlimit 200, memory cap 512MB). Use verify-lite for quicker runs.

Project Structure

signal-protocol-core/
├── src/
│   ├── lib.rs
│   ├── crypto.rs        # Abstract stubs when crypto-backend off
│   ├── keys.rs
│   ├── x3dh.rs          # #[hax_lib::include] on key functions
│   ├── double_ratchet.rs
│   ├── types.rs
│   └── error.rs
└── proofs/
    └── fstar/
        └── extraction/
            ├── AbstractCrypto.fst    # Hand-written abstract crypto
            ├── Makefile
            └── hax.fst.config.json

Hax Annotations

The Rust code uses Hax attributes to control extraction:

Attribute	Purpose
#[hax_lib::include]	Include this function in F* extraction
#[hax_lib::fstar::replace_body("...")]	Replace the function body with custom F* code (used for crypto primitives)

Functions like x3dh_initiate_internal, x3dh_respond_internal, derive_message_key, perform_dh_ratchet_step, and skip_message_keys are marked with #[hax_lib::include].

AbstractCrypto Module

The AbstractCrypto.fst module provides abstract (uninterpreted) cryptographic primitives. Instead of real implementations, these are assumed to satisfy security axioms.

Assumed Primitives

Primitive	Type	Purpose
generate_private_key	unit → private_key	Generate a fresh 32-byte private key
public_key_of_private	private_key → public_key	Derive public key from private key
dh	private_key → public_key → shared_secret	X25519 Diffie-Hellman
sign	private_key → bytes → signature	Ed25519 signature
verify	public_key → signature → bytes → bool	Ed25519 verification
hkdf_derive	salt → ikm → info → len → Result bytes	HKDF key derivation
aead_encrypt / aead_decrypt	Key, plaintext/ciphertext, AAD, nonce	AEAD encryption

Security Axioms

The module includes lemmas (assumed mathematical properties) that capture essential security:

DH Security

• Commutativity: $DH(a, B) = DH(b, A)$ when $B = \text{pub}(b)$ and $A = \text{pub}(a)$—essential for key agreement
• Determinism: Same inputs produce same output
• Correctness: Produces 32-byte shared secret for valid inputs

Signature Security

• Correctness: Valid signatures verify with the matching public key
• Unforgeability: Verification rejects signatures from wrong keys

Key Properties

• Injectivity: Different private keys yield different public keys
• Forward secrecy: Compromise of long-term key doesn't reveal past DH secrets

HKDF and AEAD

• Determinism: Same inputs produce same output
• AEAD round-trip: Decryption of encryption recovers plaintext

Signal-Specific

• X3DH key agreement: Initiator and responder derive the same shared secret
• X3DH with one-time prekey: DH4 produces matching secrets

Docker Support

For a reproducible environment:

docker compose run formal-shell

Then inside the container:

cd signal-protocol-core/proofs/fstar/extraction
make

Or run the hax-fstar target directly:

docker compose run hax-fstar

What Gets Verified

• X3DH: Key authentication, forward secrecy, key indistinguishability, mutual key agreement
• Double Ratchet: Message key uniqueness, forward secrecy after compromise, chain key integrity, out-of-order message handling

The F* type checker ensures that the extracted protocol logic is consistent with the AbstractCrypto axioms. This complements ProVerif's symbolic model checking by verifying the implementation code directly.