Publications

Papers & artifacts

CryptoBAP is developed in the open. Every paper below ships with a reproducible artifact branch in the repository.

CCS 20262026

Automated Side-Channel Analysis of Cryptographic Protocol Implementations

ACM CCS 2026

Faezeh Nasrabadi · Robert Künnemann · Hamed Nemati

Read abstractHide 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.

BibTeX

@misc{nasrabadi2026sidechannel,
  title        = {Automated Side-Channel Analysis of Cryptographic
                  Protocol Implementations},
  author       = {Nasrabadi, Faezeh and K{\"u}nnemann, Robert and Nemati, Hamed},
  year         = {2026},
  eprint       = {2511.11385},
  archivePrefix= {arXiv},
  primaryClass = {cs.CR},
  url          = {https://arxiv.org/abs/2511.11385}
}

CSF 20252025

Symbolic Parallel Composition for Multi-language Protocol Verification

38th IEEE Computer Security Foundations Symposium

Faezeh Nasrabadi · Robert Künnemann · Hamed Nemati

Read abstractHide abstract

The implementation of security protocols often combines different languages, which poses a challenge to traditional verification techniques that typically assume a single-language environment and are insufficient to handle challenges presented by the interplay of different languages. We establish principles for combining multiple programming languages operating on different atomic types using a symbolic execution semantics, which facilitates the parallel composition of labelled transition systems and improves the analysis of complex systems by streamlining communication between diverse programming languages. By treating the Dolev–Yao model as a symbolic abstraction, our approach eliminates the need for translation between different base types, such as bitstrings and Dolev–Yao terms, and provides a foundation for securing interactions in multi-language environments.

BibTeX

@inproceedings{nasrabadi2025symbolic,
  title     = {Symbolic Parallel Composition for Multi-language
               Protocol Verification},
  author    = {Nasrabadi, Faezeh and K{\"u}nnemann, Robert and Nemati, Hamed},
  booktitle = {2025 IEEE 38th Computer Security Foundations Symposium (CSF)},
  pages     = {378--393},
  year      = {2025},
  publisher = {IEEE}
}

CCS 20232023

CryptoBap: A Binary Analysis Platform for Cryptographic Protocols

ACM SIGSAC Conference on Computer and Communications Security

Faezeh Nasrabadi · Robert Künnemann · Hamed Nemati

Read abstractHide abstract

CryptoBap is a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. It works by transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. The symbolic execution resolves indirect jumps and supports bounded loops using the loop-summarization technique, which is fully automated. The extracted model is then translated into models amenable to automated verification via ProVerif and CryptoVerif using a third-party toolchain. We prove the soundness of the proposed approach and use CryptoBap to verify multiple case studies ranging from toy examples to real-world protocols, TinySSH, an implementation of SSH, and WireGuard, a modern VPN protocol.

BibTeX

@inproceedings{nasrabadi2023cryptobap,
  title     = {CryptoBap: A Binary Analysis Platform for Cryptographic
               Protocols},
  author    = {Nasrabadi, Faezeh and K{\"u}nnemann, Robert and Nemati, Hamed},
  booktitle = {Proceedings of the 2023 ACM SIGSAC Conference on Computer
               and Communications Security (CCS '23)},
  year      = {2023},
  publisher = {ACM},
  doi       = {10.1145/3576915.3623090}
}

Source

The repository

The main branch carries the current platform; each publication has its own artifact branch pinned to the state used for evaluation. A compatible version of HolBA is included, so the framework can be built and the bundled examples reproduced.

Source on GitHub

Artifact branches

Licence

Released under the GNU Affero General Public License v3.0. Commercial licences are available on request.

AGPL-3.0

Contact

nasrabadi.faezeh@gmail.com