The primitives the session model is parameterized by (all abstract).

KeyPair (core/curve.rs:320–324).

ChainKey { key: [u8; 32], index: u32 } (ratchet/keys.rs:142–145).

MessageKeyGenerator::Seed((seed, counter)) (ratchet/keys.rs:13–17, 29–31, 54–60): 32-byte seed HMAC(chain key, 0x01) and u32 counter.

MessageKeys { cipher_key, mac_key, iv, counter } (ratchet/keys.rs:91–97).

MessageKeyGenerator::generate_keys(pqr_key) on a Seed (ratchet/keys.rs:32–36) = MessageKeys::derive_keys(seed, pqr_key, counter) (:100–118): HKDF(salt = pqr_key, ikm = seed, "WhisperMessageKeys", 80) split 32/32/16, exactly HKDF.deriveMessageKeys.

ChainKey::next_chain_key (ratchet/keys.rs:165–170): key' = HMAC(key, 0x02) (the chain step Ratchet.chainHmac), index + 1. The u32 addition panics at index = u32::MAX (overflow checks are on in libsignal's release profile, Cargo.toml:250–251).

DEV-LS19 (libsignal): u32 counter, 0-based on the wire, panic at u32::MAX. ACD19's message indices are 1-based and unbounded. libsignal's counter is a u32, the wire carries i − 1, and next_chain_key panics at u32::MAX. The reductions treat an index ≥ 2³² as a structural rejection, and the theorem assumes 2(q + 1) + 25002 < 2³² (hq32). Effect: none for realistic sessions (the bound is vacuous long before, DEV-LS31).

RootKey::create_chain(self, their_ratchet_key, our_ratchet_key) (ratchet/keys.rs:199–218): the X25519 agreement (InvalidKeyAgreement if all zero, core/curve.rs:296–309) and the root KDF, via Ratchet.createChain; the new chain key has index 0.

spqr::Direction (A2B for the initiator, B2A for the recipient, ratchet.rs:86, 149).

The SPQR interface (crate spqr 1.6.0, src/lib.rs): state PQ (upstream the serialized bytes SerializedState = Vec<u8>, :43; here abstract, so a game can plug in any state machine), pq_ratchet messages as bytes (SerializedMessage = Vec<u8>, :44, they go on the wire), coins PQC:

• init dir pqrKey (spqr::initial_state, :211): the initial state from PQXDH's pqr_key; both parties use the same key (directions A2B / B2A).

• send state coins (spqr::send, :264): the new state, the message key (the HKDF salt of the message keys; none = no salt) and the pq_ratchet bytes; none = Err.

• recv state msg (spqr::recv, :355): the new state and the message key; .error true = Error::StateDecode (mapped to InvalidState), .error false = any other error (mapped to InvalidMessage, triple_ratchet.rs:242–251).

• sendPanics state coins / recvPanics state msg: spqr::send / spqr::recv panics on these inputs. libsignal is built with panic = "abort", so the session operations abort (SignalProtocolError.panic) at the call site; the values of send / recv on such inputs are never used.

No property is assumed. Upstream moves the state out of the session with mem::take (state/session.rs:677–679), leaving an empty Vec; the model leaves default : PQ ([Inhabited PQ]; for PQ = List (BitVec 8) it is [], exactly upstream).

The bytes before the MAC (serialized of SignalMessage::new before extend_from_slice(&mac), protocol.rs:93–109): versionByte ‖ protobuf { ratchet_key = Some(serialize), counter = Some, previous_counter = Some, ciphertext = Some, pq_ratchet = None if empty, addresses }.

SignalMessage::new (protocol.rs:79–128). addresses is the already serialized serialize_addresses(sender, recipient) (:91–92, 237–252): none if no addresses are passed or they are not valid service ids.

DEV-LS20 (libsignal): the wire format. ACD19 Fig. 8 sends (h, e) with e ← Enc(K, h, m). libsignal sends version ‖ protobuf{ratchet_key, counter, previous_counter, ciphertext, pq_ratchet?, addresses?} ‖ 8-byte MAC: AES-256-CBC with PKCS#7, then HMAC-SHA256 truncated to 8 bytes over the raw bytes. The receiver parses the counter before it checks the MAC. The proof models this as a per-message AEAD on the wire AEAD (lAead). Effect: constants (the 8-byte tag gives the forgery term macForgeryProb ≥ 2⁻⁶⁴, DEV-LS23).

SignalMessage::verify_mac (protocol.rs:160–173): split off the last 8 bytes and compare them with compute_mac of the rest (ct_eq). serialized.len() ≥ 9 holds for every message built by new / try_from.

SignalMessage::verify_mac_with_addresses (protocol.rs:175–212): the MAC, then, if the message carries addresses, they must equal expected = serialize_addresses(sender, recipient) (none = not serializable ⇒ reject). The wire AEAD's addressCheckPasses. The Result error of compute_mac cannot occur.

SenderChain { ratchet_key, chain_key } (double_ratchet.rs:46–50).

Receiver chain (session_structure::Chain, proto/storage.proto:11–33, double_ratchet.rs:304–309): peer ratchet public key, chain key, and stored skipped keys (newest first).

DEV-LS9 (libsignal): per-chain skipped-key stores instead of FS-AEAD instances. libsignal keeps a sender chain and up to 5 receiver chains, each storing up to 2000 skipped keys as 32-byte seeds expanded with the receiving message's SPQR salt (bounds in DEV-LS10).

RatchetState (double_ratchet.rs:31–42), with receiverChains ordered oldest first.

Run a Mut action on a field of the state (self.ratchet.m(…) from a method of the outer struct).

find_receiver_chain_key (double_ratchet.rs:257–269): the chain key of that chain; Err(missing receiver chain key) if it is None.

dh_ratchet_step (double_ratchet.rs:271–320), both half-steps, with coins the 32 bytes of KeyPair::generate(csprng):

1. missing sender chain if none (no change);

2. take the root key (now zero in self);

3. receiving half-step create_chain(their, our sender private key) (may fail: InvalidKeyAgreement, root key left zero);

4. fresh key pair; sending half-step create_chain(their, new private key) (may fail likewise);

5. previous_counter = sender index saturating_sub 1, root key, push the receiver chain (their, receiver chain key, []), evict to 5, new sender chain. Returns the receiver chain key.

take_skipped_key (double_ratchet.rs:322–344): in the chain for their (if any), find the first stored key with index = counter (position), remove it and return it; none if there is no such chain or key. (from_pb cannot fail on a Seed-form key.)

store_skipped_key (double_ratchet.rs:346–361): insert(0, key) into the chain for their (panics if there is none), then pop() the oldest if more than 2000.

set_receiver_chain_key (double_ratchet.rs:363–368): set the chain key of the chain for their (panics if there is none).

The loop while chain_key.index() < counter { store_skipped_key(their, chain_key.message_keys()); chain_key = chain_key.next_chain_key(); } (double_ratchet.rs:244–247) with fuel bounding the iterations (consumeMessageKey passes counter − index, which is exactly the number of iterations; with fuel = 0 the loop stops).

consume_message_key (double_ratchet.rs:203–253) for the receiver chain of their with chain key chainKey and message counter:

• counter < index: take_skipped_key, or DuplicatedMessage(index, counter) (no change);

• counter − index > max_forward_jumps: InvalidMessage(too far into the future) (no change);

• otherwise store the skipped keys index … counter − 1 (newest first, at most 2000), set the receiver chain key to the key after counter, return the key at counter.

ensure_receiver_chain (double_ratchet.rs:185–195): the chain key of the chain for their if there is one, else dh_ratchet_step (which consumes coins).

TripleRatchet (triple_ratchet.rs:160–165).

TripleRatchet::decrypt (triple_ratchet.rs:215–298): advances/consumes the receiver chain key (persisting on later failure), steps spqr.recv, verifies the MAC and address blob over raw bytes, AES-CBC decrypts, and commits newPqrState.

OutgoingTripleRatchet (triple_ratchet.rs:41–49).

OutgoingTripleRatchet::encrypt (triple_ratchet.rs:86–135): steps spqr.send, derives salted message keys, AES-CBC encrypts and MACs via SignalMessage.new, and advances the sender chain key (panicking at u32::MAX).

Ratchet-relevant fields of SessionState / SessionStructure (state/session.rs:141–171, proto/storage.proto:10–68).

take_ratchet_state(self_session = false) (state/session.rs:625–635) with RatchetState::from_pb (double_ratchet.rs:71–99): move the receiver chains out (left empty), copy root key, sender chain, previous counter; max_forward_jumps = MAX_FORWARD_JUMPS. (from_pb's errors are about malformed bytes, not representable here.)

TripleRatchet::from_session_state (triple_ratchet.rs:176–193): take the ratchet and SPQR states (mutating state), read the identity keys (missing remote identity key if absent).

TripleRatchet::apply_to_session_state (triple_ratchet.rs:199–202) with RatchetState::apply_to_pb (double_ratchet.rs:105–117): write root key, previous counter, sender chain, receiver chains and the SPQR state back.

try_decrypt_with_state (session_management.rs:566–606, self_session = false): build a TripleRatchet from state (which moves fields out of it), decrypt, and on success write the ratchet back and clear the unacknowledged pre-key flag. On error, state is left as from_session_state / the failed decrypt left it (the caller discards it).

The error try_decrypt_from_record returns for a failed try_decrypt_with_state with a single session: DuplicatedMessage as is (session_management.rs:432); a panic is never collected (it aborts / unwinds); every other error is collected and becomes InvalidMessage(msg_type, "decryption failed") (:436–455 for PreKey, :527–554 for Whisper after the empty previous-session loop).

try_decrypt_from_record (session_management.rs:368–556) for a record with a current session record and no previous sessions: on a clone, check the version (UnrecognizedMessageVersion, collected), run try_decrypt_with_state; store the clone only on success. A version mismatch is collected (InvalidMessage(msg_type, "decryption failed")); other errors are mapped by recordError. On error the record is unchanged.

DEV-LS16 (libsignal): reject leaves the state unchanged only through the caller's clone. ACD19 Def. 7 (A) asks that a rejected ciphertext leaves the state unchanged. libsignal's inner methods do not: on error they leave a zeroed root key or a removed skipped key. try_decrypt_from_record works on a clone and stores it only on success, so Def. 7 (A) holds at this level. Effect: none.