Hax and Rocq Verification

We use Hax to extract our Rust implementation into Rocq (formerly Coq), an interactive theorem prover and dependently-typed 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 Rocq verification.

What is Rocq?

Rocq is the successor to the Coq Proof Assistant (renamed March 2025). It uses .v files and is fully backward compatible with most Coq code. Rocq provides a mature, well-documented theorem proving environment with tactic-based proofs.

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 Rocq (via hax's into coq backend)
3. Replaces cryptographic primitives with abstract stubs when crypto-backend is disabled

Extraction Pipeline

Prerequisites

• OPAM and OCaml: sudo apt install opam, then opam init and opam switch create 5.1.1
• Rocq: opam install rocq-prover
• 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 coq

This generates Rocq files in proofs/coq/extraction/.

Makefile Workflow

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

make extract       # Extract only (no verification)
make verify        # Verify all Rocq modules
make              # Extract and verify
make verify-lite   # Verify core modules only (Crypto, Keys, Error, Types, X3dh)

Double Ratchet verification is resource-intensive. 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/
    └── coq/
        └── extraction/
            ├── AbstractCrypto.v       # Hand-written abstract crypto
            ├── Core_Extra.v           # Core library compatibility
            ├── Makefile
            ├── hax.coq.config.json
            └── Signal_protocol_core*.v   # Extracted Rocq files

Hax Annotations

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

Attribute	Purpose
#[hax_lib::include]	Include this function in Rocq 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.v module provides abstract (uninterpreted) cryptographic primitives. Instead of real implementations, these are assumed to satisfy security axioms via Parameter and Axiom declarations.

Assumed Primitives

Primitive	Type	Purpose
generate_private_key	unit → unit * bytes	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	bytes → bytes → bytes → nat → Result	HKDF key derivation
aead_encrypt / aead_decrypt	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/coq/extraction
make

Or run the Rocq targets directly:

docker compose run hax-coq      # Extract Rocq from Rust
docker compose run coq-verify   # Verify all Rocq files
docker compose run coq-shell    # Interactive Rocq shell

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 Rocq compiler ensures that the extracted protocol logic type-checks and is consistent with the AbstractCrypto axioms. This complements ProVerif's symbolic model checking by verifying the implementation code directly.

F* vs Rocq Comparison

Aspect	F*	Rocq
File Extension	.fst	.v
Compiler	fstar.exe	rocq
Parallel Build	--cache_checked_modules	rocq make -j
Axioms	assume	Parameter and Axiom
Proof Style	SMT/Z3 automated (refinement types)	Tactic-based (LEMM, apply, induction)
Community	Crypto-focused, smaller	Very large, mature (CompCert, Mathematical Components)
Learning Curve	Steep	Moderate

For F* extraction and verification, see Hax and F* Verification. For Lean 4 extraction and verification, see Hax and Lean Verification.