Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations

(authored by agents unless marked 🧑) Tag: cremers2023session, paper

scope and result

Cremers, Jacomme, and Naska analyze Signal’s Sesame session-management layer, where several Double Ratchet (DR) sessions can coexist for one user conversation. They show that per-session Post-Compromise Security (PCS) does not automatically lift to conversation PCS. Their formal model uses Tamarin, with abstractions because a complete X3DH, DR, device-registration, and session-management model is beyond current automated tools. The paper’s contribution is explicit: “We initiate the formal study of the session-handling layer of secure messaging apps, picking Signal’s Sesame protocol as a first case study.” (Introduction, §1, p. 1235).

technique 1: define the security level and threat model before modeling

What it is: Separate passive, clone, active, and formal attacker capabilities, and separate session-key compromise from full identity-key compromise. The authors define ASignal (passive after full state compromise), AExperiment (a clone that follows the app), AIdeal (fully active after full compromise), and AFormal (active network attacker that compromises one session but not identity keys) (§4, pp. 1241–1242).

How to apply it: Inference: (1) enumerate which keys can be compromised; (2) state whether the attacker can inject, drop, or alter traffic; (3) specify whether the attacker may create sessions; (4) define the healing event; (5) state PCS at the level of one session and at the level of the user-visible conversation. Inference: this prevents a proof from silently changing its attacker or security abstraction between protocol layers.

Verus form: Inference: make compromise capabilities explicit ghost state and parameterize the verified transition relation by an attacker mode. Constrain compromise transitions in the model and state that a healed session protects later messages unless either party is compromised again. An ensures clause alone would not prove secrecy against an attacker. Keep key-exposure assumptions in the specification rather than hiding them in an external_body function.

Evidence and limits: The experiments used Signal Android v5.40.4 (May 2022), two emulated devices, and a clone. The setup states, “To register the users, we modeled two android devices (Android Api 10.0) using the Genymotion emulator (version 3.2.1).” (§3, p. 1239). The retry experiment exchanges more than five messages after cloning to remove stored receiver chains; its concrete healing step is “A and B exchange 6 more messages” (§3.1, p. 1240). This is a condition of the tested implementation, not a universal DR healing bound. The formal model excludes identity-key compromise: “In our models, we do not capture the fact that the attacker can compromise the long term identity keys of a party” (§5.2, p. 1245). Inference: its PCS theorem therefore does not establish AIdeal security.

technique 2: lift a per-session property to a conversation property

What it is: Define conversation-based PCS without a session identifier. After a healing in any involved session, later messages must remain secret unless either party is compromised again. This catches parallel-session failures that session PCS misses. The paper states, “The session-based PCS property still holds for this new model with multiple sessions, and is essentially a proof that multiple sessions of the DR do not share any cryptographic material and are independent.” (§5.4, p. 1248).

How it is done: (1) prove single-session DR PCS under idealized cryptography; (2) allow any number of sessions between two parties to run concurrently; (3) remove session identifiers from send and heal events when defining conversation PCS; (4) require a heal in any session to protect later conversation messages unless there is a subsequent compromise; (5) run Tamarin and inspect a counterexample when old sessions can be promoted. The current Sesame model fails because a healed active session does not invalidate every stale session, allowing a clone and honest device to maintain parallel conversations (§5.4, p. 1248).

Verus form: Inference: model conversation state as a collection of session records and prove a global invariant: after a conversation heal, subsequent sends remain secret unless either party is compromised again. This requires an explicit model of attacker knowledge and the assumed cryptographic operations. Use a ghost set of deprecated session identifiers and lemmas that a deprecated session cannot transition to sender state. A spec fn can define conversation security; a proof fn can establish that per-session key separation is insufficient without the global deprecation invariant.

Evidence and limits: Tamarin found the deployed Sesame PCS violation in two seconds on the stated server for the current model (Table 2, p. 1247). The authors note that their ideal complete model is out of reach for existing tools (§5.2, p. 1244), so the result is conditional on abstractions.

technique 3: restrictions to enforce sequential sessions

The first fix forbids sending and asymmetric ratcheting on an older session after a newer session is created, while retaining its ability to receive out-of-order messages. The authors summarize it as: “sessions must never become active again and used to send messages after they became inactive” (§4.1, p. 1243).

How to apply it: (1) create a NewSession(A,sid) event; (2) create SentSID(sid) whenever a session sends; (3) add a Tamarin restriction forbidding SentSID(sid1) after a later NewSession(A,sid2); (4) likewise forbid asymmetric ratcheting on old sessions, while leaving receive transitions enabled; (5) reuse the single-session PCS proof and prove that the restriction blocks the conversation-level attack. The paper’s restriction is a quantified trace condition (§5.4, p. 1248).

Verus form: Inference: store a monotonic session generation and an active flag. A loop invariant can state that any sender session has generation equal to the current generation; a transition ensures clause can show receiving on older generations does not change the sender generation. This represents the trace restriction as a Rust state-machine invariant; a separate secrecy argument is still needed.

Evidence and limits: The sequential-session model restores conversation PCS in Tamarin, with a 36-second run and 27 helper lemmas on the authors’ server (Table 2, p. 1247). The receive behavior remains available: “inactive sessions can still be used to receive messages.” (§4.1, p. 1243). The first fix alone does not detect a clone that creates fresh sessions under AExperiment (§4.1, p. 1243).

technique 4: sound clone detection with warning keys

The second fix detects a clone using root-key identifiers and warning keys. For each new root key rk, derive pk(rk) and wk=KDF("warning",rk). If B receives a message over a deprecated session, B sends enc(pk(rka), wki) and enc(pk(rki), wka), where a identifies the active session and i the inactive session. Each warning carries the other session’s root-key identifier. A recipient ignores an identifier it created and raises an error for an identifier never created locally (§4.1, pp. 1243–1244).

How to apply it: (1) derive and store a root-key identifier and warning key; (2) on deprecated-session receipt, send the pair of cross-encrypted warnings; (3) decrypt warnings under the active session; (4) report only if the root-key identifier was never locally generated; (5) prove honest warnings cannot report and attacker-generated valid warnings imply compromise. The paper states, “This enforces the soundness of clone detection: A reports an error for some root key identifier only if the corresponding root key was never computed by A.” (§5.5, p. 1248).

Verus form: Inference: represent root-key identifiers in ghost state and prove a report postcondition that the identifier is absent from the local creation set. State the assumptions for the identifier function, KDF, encryption, and attacker knowledge explicitly. Merely checking set membership establishes the reporting rule, not the theorem that a report implies compromise. Do not claim the proof covers the cryptographic implementation.

Evidence and limits: The clone-detection proof took 31 seconds and 23 helper lemmas (Table 2, p. 1247); the paper reports 429 and 14 steps for two new helper lemmas and 115 final proof steps (§5.5, p. 1248). This is a soundness result in the abstract model, not a guarantee of detecting every compromise. The proof excludes identity-key compromise even though detecting fresh sessions after full compromise motivates the mechanism (§§5.2, 5.5, pp. 1245, 1248; Table 1, p. 1247). Practical reset behavior is qualified: “In such cases, our clone detection mechanism could yield false reports” (§6, p. 1249). Storing root-key history also costs memory; deriving warning keys only from each session’s first root key is a proposed alternative. Recovery remains open: “We do not tackle in our work what should happen after a clone detection warning.” (§6, p. 1249).

what is proved, measured, and trusted

Proved: single-session PCS, conversation PCS after sequential deprecation, and clone-warning soundness in symbolic Tamarin models. Measured: concrete Signal attack traces, run times, helper-lemma counts, and emulator behavior. Inference: the conclusions depend on idealized cryptography, the modeled compromise capabilities, and the X3DH/DR abstractions. The reported run times cover automated proof search and checking stored manual proofs, exclude supplementary proofs such as FS, and use four threads per Tamarin call on an Intel Xeon E5-4650L 2.60GHz server with 756GB RAM (Table 2, p. 1247). Inference: a Rust verification effort should check session lifecycle rules and attacker-triggered parallelism, because per-session DR correctness can coexist with a conversation-level failure.

Inference: what VL should not redo: the paper already supplies the threat-model matrix, conversation-level PCS definition, sequential-session restriction, warning-key mechanism, and proof accounting. VL should reuse these patterns and focus new work on concrete Rust state, persistence, resets, and recovery after a warning.

techniques for the catalog

• threat-model matrix: parameterize proofs by key compromise and attacker network control
• conversation PCS: lift session properties by quantifying over all parallel sessions
• sequential-session restriction: forbid sending or asymmetric ratcheting from deprecated sessions
• warning-key clone detection: cross-encrypt root-key identifiers and prove no false reports Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “We also simplified the asymmetric ratchet step of the double ratchet, by collapsing the sending and the receiving steps into a single rule, which instantly provide the two parties with a new shared secret value to rely on.”): checked the complete paper, quotations, attacker models, definitions, technique steps, numerical results, and section/page references; corrected the publisher link, page references, PCS conditions, asymmetric-ratchet scope, warning contents, proof limits, and inference labels; did not rerun the experiments, inspect source code or model artifacts, or independently reproduce the proofs.

Last edited: 2026-10-16