Automated Side-Channel Analysis of Cryptographic Protocol Implementations

• URL: http://arxiv.org/abs/2511.11385v2
• Date: Mon, 17 Nov 2025 15:36:51 GMT
• Title: Automated Side-Channel Analysis of Cryptographic Protocol Implementations
• Authors: Faezeh Nasrabadi, Robert Künnemann, Hamed Nemati,
• Abstract summary: 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.
• Score: 9.38081874899831
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We extract the first formal model of WhatsApp from its implementation by combining binary-level analysis (via CryptoBap) with reverse engineering (via Ghidra) to handle this large closed-source application. Using this model, we prove forward secrecy, identify a known clone-attack against post-compromise security and discover functional gaps between WhatsApp's implementation and its specification. We further introduce a methodology to analyze cryptographic protocol implementations for their resilience to side-channel attacks. This is achieved by extending the CryptoBap framework to integrate hardware leakage contracts into the protocol model, which we then pass to the state-of-the-art protocol prover, DeepSec. This enables a detailed security analysis against both functional bugs and microarchitectural side-channel attacks. Using this methodology, we identify a privacy attack in WhatsApp that allows a side-channel attacker to learn the victim's contacts and confirm a known unlinkability attack on the BAC protocol used in electronic passports. Key contributions include (1) the first formal model of WhatsApp, extracted from its binary, (2) a framework to integrate side-channel leakage contracts into protocol models for the first time, and (3) revealing critical vulnerabilities invisible to specification-based methods.

Related papers

• The Trojan Knowledge: Bypassing Commercial LLM Guardrails via Harmless Prompt Weaving and Adaptive Tree Search [58.8834056209347]
  Large language models (LLMs) remain vulnerable to jailbreak attacks that bypass safety guardrails to elicit harmful outputs.<n>We introduce the Correlated Knowledge Attack Agent (CKA-Agent), a dynamic framework that reframes jailbreaking as an adaptive, tree-structured exploration of the target model's knowledge base.
  arXiv  Detail & Related papers  (2025-12-01T07:05:23Z)
• Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
  We re-model the Needham-Schroeder protocol using an Isabelle formalism that generates sound animation.<n>Our findings reveal an uncommon but expected outcome: authenticity is preserved across all examined scenarios.<n>We have proposed a PLS-based Diffie-Hellman protocol that integrates watermarking and jamming.
  arXiv  Detail & Related papers  (2025-08-26T20:59:16Z)
• The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version) [6.595258607341775]
  We develop a methodology called *Diodon* that splits the protocol implementation into the protocol implementation and the remainder.<n>This split allows us to apply powerful semi-automated verification techniques to the security-critical Core.<n>Fully-automatic static analyses scale the verification to the entire by ensuring that the Application cannot invalidate the security properties proved for the Core.<n>We evaluate Diodon on two case studies: an implementation of the signed Diffie-Hellman key exchange and a large (100k+ LoC) production Go implementing a key exchange protocol.
  arXiv  Detail & Related papers  (2025-07-01T09:25:54Z)
• CodeChameleon: Personalized Encryption Framework for Jailbreaking Large Language Models [49.60006012946767]
  We propose CodeChameleon, a novel jailbreak framework based on personalized encryption tactics. We conduct extensive experiments on 7 Large Language Models, achieving state-of-the-art average Attack Success Rate (ASR) Remarkably, our method achieves an 86.6% ASR on GPT-4-1106.
  arXiv  Detail & Related papers  (2024-02-26T16:35: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)
• Protecting Model Adaptation from Trojans in the Unlabeled Data [120.42853706967188]
  This paper explores the potential trojan attacks on model adaptation launched by well-designed poisoning target data.<n>We propose a plug-and-play method named DiffAdapt, which can be seamlessly integrated with existing adaptation algorithms.
  arXiv  Detail & Related papers  (2024-01-11T16:42:10Z)
• Performance-lossless Black-box Model Watermarking [69.22653003059031]
  We propose a branch backdoor-based model watermarking protocol to protect model intellectual property. In addition, we analyze the potential threats to the protocol and provide a secure and feasible watermarking instance for language models.
  arXiv  Detail & Related papers  (2023-12-11T16:14:04Z)
• CryptoBap: A Binary Analysis Platform for Cryptographic Protocols [6.514727189942011]
  We introduce CryptoBap, a platform to verify weak secrecy and authentication for cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution. We prove the soundness of the proposed approach and used CryptoBap to verify multiple case studies ranging from toy examples to real-world protocols.
  arXiv  Detail & Related papers  (2023-08-28T09:41:45Z)
• Provably Secure Commitment-based Protocols over Unauthenticated Channels [0.0]
  We build a theoretic security framework to cover protocols whose characteristics may not always concur with existing models for authenticated exchanges. We propose a number of Commitment-based protocols to establish a shared secret between two parties, and study their resistance over unauthenticated channels. This means analyzing the security robustness of the protocol itself, and its robustness against Man-in-the-Middle attacks.
  arXiv  Detail & Related papers  (2023-07-28T10:35:35Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)
• Dispelling Myths on Superposition Attacks: Formal Security Model and Attack Analyses [0.0]
  We propose the first computational security model considering superposition attacks for multiparty protocols. We show that our new security model is satisfiable by proving the security of the well-known One-Time-Pad protocol. We use this newly imparted knowledge to construct the first concrete protocol for Secure Two-Party Computation that is resistant to superposition attacks.
  arXiv  Detail & Related papers  (2020-07-01T18:00:54Z)
• Mind the GAP: Security & Privacy Risks of Contact Tracing Apps [75.7995398006171]
  Google and Apple have jointly provided an API for exposure notification in order to implement decentralized contract tracing apps using Bluetooth Low Energy. We demonstrate that in real-world scenarios the GAP design is vulnerable to (i) profiling and possibly de-anonymizing persons, and (ii) relay-based wormhole attacks that basically can generate fake contacts.
  arXiv  Detail & Related papers  (2020-06-10T16:05:05Z)

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.