Hax and Lean Verification

We use Hax to extract our Rust implementation into Lean 4, a dependently-typed theorem prover and 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 Lean verification.

What is Lean 4?

Lean 4 is a functional programming language and theorem prover with a powerful dependent type system. It uses the Lake build system and has a growing ecosystem for formal verification. Lean 4's tactic-based proof style and modern tooling make it well-suited for verifying cryptographic protocols.

Hax extracts Rust code into verification-friendly formats: F*, Rocq (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 Lean 4 (via hax's into lean backend)
3. Replaces cryptographic primitives with abstract stubs when crypto-backend is disabled

Extraction Pipeline

Prerequisites

• elan: Lean version manager — curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
• Lean 4: elan toolchain install leanprover/lean4:v4.28.0-rc1 (or as specified in lean-toolchain)
• OPAM and OCaml: For the Hax engine — sudo apt install opam, then opam init and opam switch create 5.1.1
• 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 lean

This generates Lean files in proofs/lean/extraction/.

Makefile Workflow

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

make extract       # Extract only (no verification)
make patch-extraction  # Apply post-extraction patches (format!, fold compatibility)
make verify        # Patch and verify all Lean modules
make              # Extract and verify
make verify-lite   # Verify core modules only (AbstractCrypto, skips Double Ratchet)

Lean extraction requires post-extraction patches before verification. The patch-extraction target applies sed fixes for format! compatibility and runs patch_fold.pl to handle iterator fold patterns that Hax extracts in a form Lean cannot compile. Use verify-lite for quicker runs when skipping Double Ratchet.

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/
    └── lean/
        ├── lean-toolchain           # leanprover/lean4:v4.28.0-rc1
        ├── lakefile.toml            # Lake config, depends on Hax Lean lib
        └── extraction/
            ├── AbstractCrypto.lean  # Hand-written abstract crypto
            ├── Makefile
            ├── patch_fold.pl        # Post-extraction patch for fold
            └── signal_protocol_core.lean  # Extracted by hax

The lakefile.toml depends on the Hax Lean library at ../../../hax-upstream/hax-lib/proof-libs/lean.

Hax Annotations

The Rust code uses the same Hax attributes as for F* and Rocq extraction:

Attribute	Purpose
#[hax_lib::include]	Include this function in Lean extraction
#[hax_lib::fstar::replace_body("...")]	Replace the function body with custom 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.lean module provides abstract (uninterpreted) cryptographic primitives. Instead of real implementations, these are assumed to satisfy security axioms via axiom declarations.

Assumed Primitives

Primitive	Type	Purpose
generatePrivateKey	Unit → PrivateKey	Generate a fresh 32-byte private key
publicKeyOfPrivate	PrivateKey → PublicKey	Derive public key from private key
dh	PrivateKey → PublicKey → SharedSecret	X25519 Diffie-Hellman
sign	PrivateKey → Bytes → Signature	Ed25519 signature
verify	PublicKey → Signature → Bytes → Bool	Ed25519 verification
hkdfDerive	Bytes → Bytes → Bytes → Nat → Except String Bytes	HKDF key derivation
aeadEncrypt / aeadDecrypt	Key, plaintext/ciphertext, AAD, nonce	AEAD encryption

Security Axioms

The module includes axioms (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/lean/extraction
make

Or run the Lean targets directly:

docker compose run hax-lean    # Extract Lean from Rust
docker compose run lean-verify # Verify all Lean files (lake build)

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 Lean type checker (via lake build) 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.

Lean-Specific Notes

• Post-extraction patches: The Lean backend extracts some Rust patterns (e.g. format!, iterator fold) in forms that require manual patches. The Makefile applies these automatically via patch-extraction.
• Lake build: Verification uses Lake rather than invoking lean directly; Lake manages dependencies including the Hax Lean library.
• Hax Lean library: The lakefile.toml references hax-upstream/hax-lib/proof-libs/lean; ensure the Hax upstream repo is cloned at the expected path.

For F* extraction and verification, see Hax and F* Verification. For Rocq (Coq) extraction and verification, see Hax and Rocq Verification.