Implementation Overview

Understanding the Rust implementation structure helps clarify what is being formally verified. This document describes the dual-crate architecture, the role of the crypto-backend feature flag, and the protocol flows for X3DH and Double Ratchet.

Dual-Crate Architecture

The implementation is split into two crates with different purposes:

Crate	Purpose
signal-protocol-wasm	Production build with real cryptography (x25519-dalek, ed25519-dalek, aes-gcm). Compiles to WebAssembly for browser use. Includes JavaScript bindings and Storybook demos.
signal-protocol-core	Core protocol logic shared by both production and verification. When crypto-backend is disabled, crypto calls are replaced with abstract stubs suitable for Hax/F* extraction.

The crypto-backend Feature Flag

The crypto-backend feature controls whether the implementation uses real cryptographic primitives or abstract ones:

• Enabled (default): Uses x25519-dalek for ECDH, ed25519-dalek for signatures, aes-gcm for encryption. This is the production configuration.
• Disabled: Crypto functions are replaced with F* code via #[hax_lib::fstar::replace_body(...)]. Required for Hax extraction—the extracted F* code uses AbstractCrypto.fst primitives.

Module Map

The core crate is organized into these modules:

Module	File	Role
crypto	crypto.rs	X25519 ECDH, HKDF, Ed25519 sign/verify; abstract stubs when crypto-backend disabled
keys	keys.rs	Identity key, signed prekey, one-time prekey, ephemeral key generation
x3dh	x3dh.rs	X3DH initiate and respond; 3–4 DH operations, HKDF derivation
double_ratchet	double_ratchet.rs	Double Ratchet state, encrypt/decrypt, DH ratchet, skipped message keys
types	types.rs	KeyPair, X3DHResult, EncryptionResult
error	error.rs	SignalError variants

X3DH Key Agreement Flow

X3DH (Extended Triple Diffie-Hellman) establishes a shared secret between Alice (initiator) and Bob (responder). The protocol combines up to four Diffie-Hellman operations.

The Four DH Operations

From Alice's perspective (initiator), the DH operations are:

$$\begin{aligned} DH_1 &= DH(IK_A, SPK_B) \quad \text{(Identity $\times$ Signed Prekey)} \\ DH_2 &= DH(EK_A, IK_B) \quad \text{(Ephemeral $\times$ Identity)} \\ DH_3 &= DH(EK_A, SPK_B) \quad \text{(Ephemeral $\times$ Signed Prekey)} \\ DH_4 &= DH(EK_A, OPK_B) \quad \text{(Ephemeral $\times$ One-Time Prekey, optional)} \end{aligned}$$

Where $IK$ = identity key, $SPK$ = signed prekey, $EK$ = ephemeral key, $OPK$ = one-time prekey.

HKDF Derivation

The concatenated DH outputs are passed through HKDF (HMAC-based Key Derivation Function):

$$\text{shared\_secret} = \text{HKDF}(\text{salt}, DH_1 \| DH_2 \| DH_3 \| DH_4, \text{info})$$

With constants: salt = Signal_X3DH_Salt, info = Signal_X3DH_Key_Derivation. Both parties compute the same shared secret because $DH(a, B) = DH(b, A)$ for Diffie-Hellman.

Double Ratchet Flow

Once X3DH produces a shared secret, the Double Ratchet uses it as the initial root key. The algorithm has two ratcheting mechanisms:

Symmetric-Key Ratchet (Chain Keys)

Each message derives a unique message key from the current chain key, then advances the chain:

$$\text{message\_key} = \text{HKDF}(\text{Signal\_Message\_Salt}, \text{chain\_key}, \text{info})$$ $$\text{next\_chain\_key} = \text{HKDF}(\text{Signal\_Chain\_Salt}, \text{chain\_key}, \text{info})$$

DH Ratchet (Root Key Updates)

When a party receives a new DH public key from the peer, they perform a DH ratchet step:

1. Compute $DH(\text{my\_private}, \text{remote\_public})$
2. Derive new root key and receiving chain key via HKDF with salt Signal_DH_Ratchet
3. Generate a new DH key pair for sending
4. Derive new root key and sending chain key

This provides break-in recovery: even if keys are compromised, the next DH ratchet produces fresh keys.

Key Derivation Constants

Use Case	Salt	Info
DH ratchet	Signal_DH_Ratchet	(combined with DH output)
Initial chain	Signal_Initial_Chain	Signal_DoubleRatchet_ChainKey
Message key	Signal_Message_Salt	Signal_DoubleRatchet_MessageKey
Advance chain	Signal_Chain_Salt	Signal_DoubleRatchet_ChainKey

What Gets Verified

• ProVerif: Models mirror these flows; verifies key secrecy, DH order, forward secrecy, post-compromise security
• Hax/F*: Extracts x3dh_initiate_internal, x3dh_respond_internal, derive_message_key, perform_dh_ratchet_step, and related functions; verifies against AbstractCrypto axioms

For protocol concepts in more depth, see the P2P Signal Protocol documentation.