[Submitted on 14 Nov 2025 (v1), last revised 30 Jul 2026 (this version, v4)]

View PDF HTML (experimental)

Abstract:Formal verification of cryptographic protocols typically relies on symbolic models that abstract away compiled code and microarchitectural side channels, leaving a gap between verified specifications and deployed executables. We present a toolchain that extracts protocol-relevant models from real binaries and analyzes them under explicit leakage contracts for constant-time and Spectre-PHT-style speculative observations. Starting from a selected binary region, we lift machine code to an intermediate representation, instrument it with leakage contracts, symbolically execute it to obtain event/observation traces, and translate these traces into Sapic+ for analysis with Tamarin, ProVerif, and DeepSec.
As case studies, we extract models of WhatsApp Desktop's session-management and double-ratchet components from its binary and analyze forward secrecy and post-compromise security under a state-cloning compromise. For side-channel analysis, we study the Basic Access Control (BAC) protocol used in e-passports and WhatsApp's session establishment. Under our observation models, we identify an instruction-cache side channel in WhatsApp Desktop enabling social-graph inference, and we reproduce known unlinkability issues in BAC under microarchitectural observations.

Submission history

From: Faezeh Nasrabadi [view email]
[v1] Fri, 14 Nov 2025 15:13:49 UTC (639 KB)
[v2] Mon, 17 Nov 2025 15:36:51 UTC (639 KB)
[v3] Thu, 7 May 2026 15:28:59 UTC (674 KB)
[v4] Thu, 30 Jul 2026 12:37:51 UTC (717 KB)