2025/11/14 by Faezeh Nasrabadi, Nasrabadi, Faezeh, Robert Künnemann +3
Computer Science · #Advanced Authentication Protocols Security #Cryptographic Implementations and Security #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Security and Verification in Computing #cs.CR
paper · pdf · doi:10.48550/arxiv.2511.11385
15 pages. To appear in the Proceedings of the 2026 ACM SIGSAC Conference on Computer and Communications Security (CCS'26)
openalex publication_date 2025/11/14 · openalex created_date 2025/11/18 · openalex updated_date 2026/07/28 · arxiv created 2026/07/30 · arxiv updated 2026/07/31
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.