Implementation Nuances

This document covers the HKDF constants used throughout the implementation, design decisions, and known limitations of the formal verification. These details are important for understanding how the implementation aligns with the ProVerif and Hax/F* models.

HKDF Constants Reference

HKDF (HMAC-based Key Derivation Function) is used to derive keys from shared secrets. The Rust implementation uses the hkdf crate pattern:

let hkdf = Hkdf::<Sha256>::new(Some(salt), input_keying_material);
hkdf.expand(info, &mut output);

ProVerif models this as a single 3-argument function: hkdf(salt, ikm, info).

X3DH Constants

Parameter	Value	Location
Salt	Signal_X3DH_Salt	x3dh.rs
Info	Signal_X3DH_Key_Derivation	x3dh.rs

The shared secret is derived as:

$$\text{shared\_secret} = \text{HKDF}(\text{Signal\_X3DH\_Salt}, DH_1 \| DH_2 \| DH_3 \| DH_4, \text{Signal\_X3DH\_Key\_Derivation})$$

Double Ratchet Constants

Use Case	Salt	Info String
X3DH handshake	Signal_X3DH_Salt	Signal_X3DH_Key_Derivation
DH ratchet	Signal_DH_Ratchet	(combined with DH output)
Initial chain key	Signal_Initial_Chain	Signal_DoubleRatchet_ChainKey
Derive message key	Signal_Message_Salt	Signal_DoubleRatchet_MessageKey
Advance chain key	Signal_Chain_Salt	Signal_DoubleRatchet_ChainKey

AAD Format

AAD (Additional Authenticated Data) is data that is authenticated but not encrypted. It binds the ciphertext to context, preventing tampering. For Double Ratchet message encryption:

$$\text{AAD} = DH\_public\_key \| message\_number \| previous\_chain\_length$$

Where:

• $DH\_public\_key$: The sender's current DH public key (32 bytes)
• $message\_number$: The message index in the current chain
• $previous\_chain\_length$: Length of the previous sending chain (for out-of-order handling)

This format ensures that messages cannot be replayed or reordered without detection.

Skipped Message Keys

When messages arrive out of order, the Double Ratchet must derive and store "skipped" message keys for messages that have not yet arrived. For example, if message 3 arrives before messages 1 and 2, the receiver must derive keys for 1 and 2, store them, and use the key for 3 to decrypt.

Key Storage

• Format: {dh_public_key_hex}:{message_number} (e.g., a1b2c3...:5)
• Max skipped: 1000 message keys (configurable via MAX_SKIPPED_MESSAGE_KEYS)
• Storage: BTreeMap for deterministic ordering

If more than 1000 messages are skipped, the implementation returns an error to prevent unbounded memory use and potential abuse.

Design Decisions

3-DH vs 4-DH (One-Time Prekey)

The full X3DH specification includes an optional one-time prekey (OPK) for the fourth DH operation. Our implementation supports both:

• 3-DH: When no one-time prekey is available (e.g., in P2P where there is no server to store OPKs)
• 4-DH: When a one-time prekey is provided (e.g., in server-based deployments)

The one-time prekey provides additional forward secrecy for the very first message. In P2P, the ephemeral key in DH2 and DH3 already provides forward secrecy, and Double Ratchet takes over immediately.

ProVerif vs CryptoVerif

We chose ProVerif over CryptoVerif because ProVerif can model:

• All 4 X3DH DH operations in the correct order
• Double Ratchet state transitions
• Forward secrecy and post-compromise security

CryptoVerif has limitations in these areas (see ProVerif Verification).

Dual-Crate Architecture

Splitting signal-protocol-core (verification-friendly) from signal-protocol-wasm (production) allows:

• Hax extraction without pulling in real crypto dependencies
• ProVerif models that mirror the core logic
• Single source of truth for protocol behavior

Known Limitations

End-to-End Correspondence

The signal_protocol_complete.pv ProVerif model does not prove that the X3DH handshake output is correctly passed to the Double Ratchet. The processes are not linked by a channel, so full end-to-end correspondence remains unproven.

Double Ratchet F* Verification Cost

F* verification of the Double Ratchet module is resource-intensive:

• Requires --z3rlimit 200 and higher fuel settings
• Memory cap of 512MB
• make verify-lite skips Double Ratchet for faster iteration

Hax Dependencies

Hax extraction requires:

• hax-upstream (cloned separately, typically gitignored)
• HAX_PROOF_LIBS from hax-upstream/hax-lib/proof-libs/fstar
• Optional HACL* at ~/.hax/hacl_home for concrete crypto primitives

Quick Reference Table

Aspect	Value
X3DH salt	Signal_X3DH_Salt
X3DH info	Signal_X3DH_Key_Derivation
DH ratchet salt	Signal_DH_Ratchet
Initial chain salt	Signal_Initial_Chain
Message key salt	Signal_Message_Salt
Chain advance salt	Signal_Chain_Salt
Chain key info	Signal_DoubleRatchet_ChainKey
Message key info	Signal_DoubleRatchet_MessageKey
AAD format	DH_pubkey | msg_num | prev_chain_len
Max skipped keys	1000

For the authoritative reference, see the signal-protocol formal-proofs repository.