The Signal protocol secures daily messages for billions of people across WhatsApp, Signal Desktop, Facebook Messenger, and Google Messages. Years of formal analysis in the computational and Dolev-Yao settings have produced strong security guarantees for the protocol itself. But a persistent gap separates what the specification promises and what the implementation actually does at runtime. Bugs, undocumented deviations, and incomplete models of the on-the-wire behavior can silently break the contract. Moustafa Said, Aurora Naska, Kevin Morio, and Robert Künnemann from CISPA Helmholtz Center tackle this gap head-on, applying a runtime monitor called SpecMon to two production messaging apps and producing formal models detailed enough for both monitoring and verification.

The Verification Gap in Messaging Security

Formal verification tools like Tamarin and ProVerif have analyzed the Signal protocol extensively. But keeping verification tractable forces researchers to abstract away protocol details: message formats, session management, key derivation steps, and implementation-specific calling conventions all get folded into simplified models. What remains unverified is precisely the boundary where theory meets practice. An implementation might skip a security-relevant step, use a different cryptographic primitive, or introduce a bug that no formal model ever considered. WhatsApp, owned by Meta (named in the NSA's PRISM disclosures), amplifies this concern: its closed-source nature makes independent verification of protocol conformance especially difficult.

Existing approaches to bridging this gap, such as code verification, verified compilers, type checking, and model extraction, are either static and labor-intensive or limited to small implementations. SpecMon offers a different path: a runtime monitor that checks whether observed execution traces conform to a formal multiset-rewrite model during actual protocol runs. Within the bounds of the Dolev-Yao threat model and trusted event extraction, guarantees of the formal model transfer to accepted implementation traces. The question this paper answers is whether that approach works at the scale of real messaging applications.

How SpecMon Bridges Formal Models and Runtime Events

SpecMon and Tamarin share multiset-rewrite rules (MSRs) as their specification language. A rule has a premise (multiset of facts to match), actions (labels for the transition), and a conclusion (multiset of facts to produce). In Tamarin, terms are symbolic Dolev-Yao terms like senc(m, k) whose meaning comes from user-defined equations. Tamarin reasons about symbolic traces generated by these rules under a network attacker to verify security properties.

SpecMon works differently. It observes concrete bitstrings from an implementation and checks whether each observed event can be explained by some rule in the model. A rule annotation called a trigger links an observed program event (a function call with concrete arguments and return value) to the rule that should fire. Since monitor events carry bitstrings rather than symbolic terms, the monitor cannot pattern-match on term structure the way Tamarin can. Instead, format strings specify how bitstrings map to the symbolic message structure. This lets one model file serve both purposes: Tamarin verifies trace properties, while SpecMon checks conformance of real traces against the same rules.

The monitor maintains a set of configurations, each representing a possible current state. When several rules could explain an event, SpecMon keeps all corresponding configurations until later events resolve the ambiguity. SpecMon's soundness theorem guarantees that for any accepted event stream (where freshly generated values are unique), there exists an abstraction from bitstrings to symbolic terms and a corresponding symbolic trace of the same model. This connects Tamarin proofs directly to monitored executions within the stated scope.

The team extended SpecMon in two directions to handle these case studies. First, they added support for cryptographic computations whose return values are never reused later in the model, and for recursive evaluation of nested format strings. Second, they improved the execution engine: reduced repeated work in rule matching, improved conflict-set computation to discard impossible states earlier, and shared memory representations of terms and facts. These changes made the same modeling approach practical for larger rule sets and concurrent sessions.

Instrumenting Signal Desktop and WhatsApp Web

The first practical challenge is extracting the right events from production applications. The team used two instrumentation strategies depending on source-code availability.

For Signal Desktop, an open-source TypeScript application, they adopted the annotated-library approach. Signal clients use libsignal, a Rust library exposed to JavaScript. The team annotated the cryptographic functions appearing in the DR and X3DH models: symmetric encryption, decryption, hashing, HKDF, ECDH operations, and key generation. Network events came from WebSocket handlers (onmessage for incoming, send_request for outgoing). The browser's WebSocket and TLS stack, or Chromium's networking stack bundled with Electron, is trusted at the transport layer.

For WhatsApp Web, a closed-source application with minified JavaScript, the team used Chrome DevTools. WhatsApp communicates over WebSockets and uses a modified version of libsignal. The team identified cryptographic components by matching function names observed at runtime against those described in Signal's white paper. They intercepted these functions via the debugger, stepped into them to analyze their logic, then overrode them to log event traces. Stack traces at the WebSocket invocation point distinguished Signal-protocol-relevant calls from unrelated traffic.

Both applications store session state persistently. Signal Desktop uses an encrypted SQLite database (SQLCipher), and WhatsApp Web uses IndexedDB. The team wrote extraction scripts to read session keys from each store and feed them to the monitor as pre-traces, initializing the monitor's state with the root key, ratchet key pairs, chain keys, and base keys for each session.

The trust boundary for monitoring is explicitly scoped. The team trusts the instrumentation code, the event aggregator, the browser's WebSocket and TLS stack, and the pre-trace initialization. Defenses against malicious applications are out of scope. The monitor catches observable divergences: incorrectly sequenced cryptographic operations, message-format mismatches, logical errors, invalid state-machine transitions, and visible cryptographic misuse. It cannot detect side channels, memory leaks, storage behavior, or errors on unexercised code paths.

Deriving the Most Detailed Signal Model to Date

The Signal Desktop model starts from two existing Tamarin models: the Double Ratchet model by Cremers et al. (2023) and the X3DH model from albert. The team merges and extends these to cover the actual implementation. Key extensions include:

  • Post-quantum ML-KEM keys used during PQXDH session initialization, the successor to X3DH that Signal now supports.
  • Explicit modeling of the initial DH ratchet step before the first message. The original Sesame model abstracts session setup by initializing a chain key directly from a fresh root key, but in Signal Desktop the initiator first performs a DH ratchet step with the recipient's signed prekey, updating the root key and deriving the sending chain key. SpecMon rejected traces from the simpler model, forcing this addition.
  • Cipher-key derivation from chain keys. Rather than encrypting directly with the chain key, Signal derives a separate message key via HKDF.
  • Sealed Sender, a mechanism that hides the sender's identity from the server. Neither the original DR nor X3DH model covered this. The team added rules for the sealed-send operation (encrypting the sender's identity key using the recipient's public key and an ephemeral key) and sealed-receive (decrypting using the corresponding private keys).

The final model contains rules for: Initiator, Responder, Prekey, Sender symmetric ratchet, Receiver symmetric ratchet, Asymmetric (DH) ratchet, Sealed send, and Sealed receive. Format strings map to Protocol Buffers definitions used in Signal Desktop's wire format. This is the most detailed Signal model produced to date, covering session management, post-quantum key exchange, the Double Ratchet, and sender anonymity.

Deriving the First WhatsApp Web Model

For WhatsApp Web, no prior formal model existed. The team derived one directly from recorded implementation traces. They used a fuzzer to generate diverse communication patterns: starting new conversations, sending and receiving batches of consecutive messages, reordering messages, skipping messages, and triggering session-loss retries. This produced traces covering the main protocol behaviors.

The WhatsApp model covers X3DH (both initiator and responder), the symmetric ratchet (sender and receiver), and the asymmetric DH ratchet. It omits Sealed Sender and PQXDH, reflecting WhatsApp's current feature set. Format strings were derived from Protocol Buffers definitions observed in the traces. A single WebSocket BLOB can bundle multiple SignalMessage objects (one per recipient device), so the event aggregator decodes each bundle and emits individual SignalMessage events to the monitor.

Two Undocumented Differences Between Signal and WhatsApp

Monitoring surfaced behavioral differences between the two applications that had not been formally documented.

The first concerns read receipts. WhatsApp Web transmits read-receipt messages outside the Double Ratchet encryption layer. When a user opens a chat, the client sends a server-visible presence message; the server then decides whether to deliver a read receipt. In Signal Desktop, read receipts participate in the encrypted message exchange and can trigger DH ratchets. This means WhatsApp performs DH ratchets less frequently than Signal for comparable user interaction patterns. The asymmetric ratchet mixes fresh DH material into the root key, which affects post-compromise recovery timing. The team does not claim this weakens WhatsApp's security outright, since actual healing also depends on how long old key material persists in memory and storage, which the methodology does not observe. But the difference in ratchet frequency is real and documented for the first time at the model level.

The second difference is the absence of PQXDH and Sealed Sender in WhatsApp Web. These are known feature-adoption differences, but the contribution here is surfacing them at the model level and documenting their behavioral consequences through runtime monitoring.

Evaluation: Validation, Fault Injection, and Performance

The team validated both models by monitoring a party (Monique) communicating with an unmonitored partner (Parker) across six action types: new conversations, sending consecutive messages, receiving consecutive messages, reordering messages, skipping messages, and session-loss retries. A random fuzzer produced continuous streams of these actions with uniform probability. For Signal Desktop, this produced about 900 messages totaling 25 MB; for WhatsApp Web, about 400 messages totaling 6.5 MB. Both models handled all traces without failure.

Stress testing with up to 5,000 consecutive messages per session (Signal Desktop caps skipped messages per chain at 2,000) also passed. Fault injection experiments deliberately injected incorrect ratchet public keys, wrong ciphertexts, swapped ciphertexts, and incorrect MACs. In each case, SpecMon correctly rejected the faulted traces, confirming that the models detect these classes of security violations. The team also verified that the monitor accepts valid messages even when some parameters (like IVs or padding) differ from the model, since unused randomness and inputs do not affect modeled behavior.

Performance measurements showed low overhead. The team does not report precise numbers in the abstract, but characterizes the monitoring as efficient for real-world applications in their measured setting. The full model development, instrumentation, fuzzing, and experiments for WhatsApp Web took three person-weeks, demonstrating that the methodology is practical for quick model extraction.

Formal Verification Results

Using Tamarin, the team verified authentication and secrecy properties for both models under three threat models: one for Signal, one for WhatsApp, and one for post-compromise security (PCS). For the initial root key, authentication and secrecy hold under both the Signal and WhatsApp threat models. The authentication guarantee does not cover a DH break before the responder completes the handshake, which matches known impossibility results.

Both models reproduce the known conversation-PCS counterexample from Cremers et al. (2023) and the impossibility result from Cremers, Movie, and Nuncio (2025): session management policies that allow session deletion or replacement prevent certain PCS properties from holding. Sealed Sender is monitored for fidelity but not separately verified. The analysis confirms that the monitoring models and verification models, while sharing the same MSR language, can diverge in scope, and the team makes this divergence explicit through the model structure.

Limitations and What This Means for Developers

The methodology trusts the instrumentation and the transport layer. It cannot catch behaviors outside the event stream, side channels, memory safety issues, storage behavior, or errors on unexercised code paths. The monitor checks that a sent message is permitted, not that it is eventually sent. Long-term production monitoring would require automating the currently manual instrumentation.

For working developers, the practical implications are concrete. Monitorable MSR models function as executable protocol documentation that stays in sync with the implementation. They can be integrated into continuous integration pipelines as an in-depth testing tool, catching protocol-level regressions as code evolves. The artifacts, including annotated libraries and trace-rewriting rules, are reusable for other Signal-based applications. The three-person-week timeline for the WhatsApp Web case study suggests that applying this methodology to a new messaging application is within reach for a small security team.

More broadly, maintaining closely related monitoring and verification variants of one MSR model creates a shared validation point. Accepted traces conform to the monitorable variant within stated trust boundaries, while documented transformations connect that variant to the model used for proof. This makes the remaining abstraction gap explicit and permits both variants to be updated as the implementation evolves.

Read the paper on arXiv