From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp

• URL: http://arxiv.org/abs/2609.11882v2
• Date: Sat, 12 Sep 2026 16:14:42 GMT
• Title: From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
• Abstract summary: We develop a model of WhatsApp Web's implementation of the Signal protocol.<n>For the core components of the Signal protocol, we verify authentication and secrecy properties.<n>Monitoring reveals previously undocumented differences between the original libsignal library and WhatsApp's fork.
• Score: 8.86750495352076
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The Signal protocol is a prominent messaging protocol that secures communication for billions of users. It powers WhatsApp, the most widely used messaging application worldwide, and the Signal app, popular among privacy-conscious users. Extensive research in the computational and Dolev-Yao settings provides strong formal security guarantees for the protocol itself. However, a gap remains between the guarantees of the protocol specification and the implementation's actual behavior at runtime. In this work, we bridge this gap by applying SpecMon, a recently proposed runtime monitor, to check whether observed executions conform to formal protocol models. To this end, we instrument two applications (WhatsApp Web and Signal Desktop) to capture their interactions with the network and the cryptographic components. Using this instrumentation, we develop two multiset-rewrite models that are compatible with Tamarin, thus enabling verification. We derive the first model of WhatsApp Web's implementation of the Signal protocol and the most detailed model to date of Signal's original protocol. Monitoring establishes that observed executions conform to these models, relative to the trusted event extraction and the symbolic abstraction. For the core components of the Signal protocol, we verify authentication and secrecy properties. Finally, monitoring reveals previously undocumented differences between the original libsignal library and WhatsApp's fork. We evaluate our methodology and demonstrate its reproducibility. Developing the WhatsApp Web model, instrumenting the app, adding fuzzing, and running the experiments took three person-weeks. We also demonstrate efficient monitoring of real-world applications and detection of deliberately injected security faults, with low overhead in our measured setting.

Related papers

• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation [0.0]
  We present a novel language-first method for verification of trace properties using a domain-specific language for protocol implementations.<n>We target the Tamarin prover for verification, and we prove that verified universal trace properties translate back to the implementation.<n>We use our tool to implement and generate accurate models for a signed Diffie-Hellman protocol, and for the WireGuard VPN protocol.
  arXiv  Detail & Related papers  (2026-06-18T08:34:17Z)
• A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
  This study develops a technical taxonomy to classify and analyze large language models (LLMs) agent communication protocols.<n>The framework guides protocol selection and highlights open research gaps such as privacy and policy enforcement.
  arXiv  Detail & Related papers  (2026-06-17T14:45:20Z)
• Autogenesis: A Self-Evolving Agent Protocol [60.15939127351914]
  We introduce Autogenesis Protocol (AGP), a self evolution protocol that decouples what evolves from how evolution occurs.<n>We present Autogenesis System (AGS), a self-evolving multi-agent system that dynamically instantiates, retrieves, and refines protocol-registered resources during execution.
  arXiv  Detail & Related papers  (2026-04-16T14:04:06Z)
• Automated Side-Channel Analysis of Cryptographic Protocol Implementations [9.38081874899831]
  We extract the first formal model of WhatsApp from its implementation.<n>We identify a known clone-attack against post-compromise security.<n>We introduce a methodology to analyze cryptographic protocol implementations for their resilience to side-channel attacks.
  arXiv  Detail & Related papers  (2025-11-14T15:13:49Z)
• Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
  We study adaptive attacks by an untrusted model that knows the protocol and the monitor model.<n>We instantiate a simple adaptive attack vector by which the attacker embeds publicly known or zero-shot prompt injections in the model outputs.
  arXiv  Detail & Related papers  (2025-10-10T15:12:44Z)
• LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
  Faults in protocol behavior can lead to vulnerabilities and system failures.<n>A common approach to protocol testing involves constructing Markovian models that capture the state transitions and expected behaviors of the protocol.<n>We propose a novel method that leverages large language models (LLMs) to automatically generate sequences for testing network protocol implementations.
  arXiv  Detail & Related papers  (2025-08-03T13:16:18Z)
• What If We Had Used a Different App? Reliable Counterfactual KPI Analysis in Wireless Systems [52.499838151272016]
  This paper addresses the problem of estimating the values of traffic that would have been obtained if a different app had been implemented by the RAN.<n>We propose a conformal-prediction-based counterfactual analysis method for wireless systems.
  arXiv  Detail & Related papers  (2024-09-30T18:47:26Z)
• SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols [5.202524136984542]
  We instrument the networking and cryptographic library the application uses to obtain a stream of events. We then use an efficient algorithm to match these observations to traces that are valid in the specification model.
  arXiv  Detail & Related papers  (2024-09-04T17:54:29Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems.
  arXiv  Detail & Related papers  (2024-05-09T19:57:59Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.