pith. the verified trust layer for science. sign in

arxiv: 2511.11385 · v3 · submitted 2025-11-14 · 💻 cs.CR

Automated Side-Channel Analysis of Cryptographic Protocol Implementations

Faezeh Nasrabadi , Robert K\"unnemann , Hamed Nemati This is my paper

Pith reviewed 2026-05-17 22:09 UTC · model grok-4.3

classification 💻 cs.CR
keywords side-channel analysisbinary liftingcryptographic protocolsformal verificationTamarinSpectreconstant-timeWhatsApp security
0
0 comments X p. Extension

The pith

A toolchain lifts real cryptographic binaries to symbolic models and checks them for leaks under explicit constant-time and speculative observation contracts.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops an automated toolchain that starts from selected regions in compiled binaries, lifts the machine code to an intermediate representation, and instruments it with leakage contracts modeling constant-time execution and Spectre-PHT style speculation. Symbolic execution then produces event and observation traces that are translated into the Sapic language for analysis in Tamarin, ProVerif, and DeepSec. The authors apply this to WhatsApp Desktop session management and double-ratchet code to verify forward secrecy and post-compromise security under state-cloning compromises, and to the BAC protocol in e-passports plus WhatsApp session establishment to detect an instruction-cache side channel enabling social-graph inference and to reproduce known unlinkability problems.

Core claim

Starting from a selected binary region, the toolchain lifts machine code to an intermediate representation, instruments it with leakage contracts, symbolically executes the instrumented code to obtain event and observation traces, and translates the traces into Sapic for analysis with Tamarin, ProVerif, and DeepSec. Case studies extract models of WhatsApp Desktop session-management and double-ratchet components to analyze forward secrecy and post-compromise security under state-cloning compromise, and examine the Basic Access Control protocol and WhatsApp session establishment under microarchitectural observations, identifying an instruction-cache side channel and reproducing unlinkability l

What carries the argument

The toolchain that lifts machine code to an IR, instruments it with leakage contracts for constant-time and Spectre-PHT observations, generates traces via symbolic execution, and translates them into Sapic for formal protocol analysis.

If this is right

  • Forward secrecy and post-compromise security properties can be checked for WhatsApp's double-ratchet implementation even when an adversary can clone protocol state and observe microarchitectural leaks.
  • An instruction-cache side channel in WhatsApp Desktop allows inference of the social graph under the modeled observation contracts.
  • The BAC protocol in e-passports exhibits known unlinkability violations once microarchitectural observations are included in the analysis.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same lifting-and-contract approach could be applied to other cryptographic libraries to check side-channel resilience before deployment.
  • Extending the leakage contracts to additional microarchitectural effects such as cache-timing or branch-predictor state would broaden the class of detectable leaks.
  • Combining the extracted models with hardware-specific simulators could provide more precise bounds on the practical impact of the identified side channels.

Load-bearing premise

The binary lifting step together with the chosen leakage contracts must accurately capture the microarchitectural observations that would occur on real hardware without introducing spurious leaks or missing real ones.

What would settle it

Direct measurement of instruction-cache timing or speculative execution behavior on the actual WhatsApp Desktop binary running on target hardware, checking whether the leaks predicted by the toolchain match the observed side-channel behavior.

Figures

Figures reproduced from arXiv: 2511.11385 by Faezeh Nasrabadi, Hamed Nemati, Robert K\"unnemann.

Figure 1
Figure 1. Figure 1: BIR’s syntax thors in March 2025. Meta has confirmed that the application is vulnerable to these identified attacks. II. BACKGROUND We build on CRYPTOBAP [2], [3], a binary analysis frame￾work that extends security protocol verification to machine code to eliminate the need to trust compilers. CRYPTOBAP ex￾tends the HolBA framework [12] to verify ARMv8 and RISC￾V machine code crypto protocols. It achieves … view at source ↗
Figure 2
Figure 2. Figure 2: A fragment of the syntax of SAPIC+ process calculus. In this figure, e, t1, t2 ∈ T , n ∈ Npriv, x ∈ V. reachable states arising from an initial symbolic state. HolBA’s symbolic execution allows for verifying functional correctness, but not (directly) protocol security, as it lacks a suitable attacker model and concurrent behavior. CRYPTOBAP bridges this gap by extracting formal models of the protocols from… view at source ↗
Figure 3
Figure 3. Figure 3: The Spectre V1 example instrumented via Mct and Mspec. We marked shadow observations with ⋆. interference [27]. Let s ∈ S be a system state, including microarchitectural components like caches, traces : T 7→ 2 O be a function to extract the sequence of observations from a given execution trace τ ∈ T, and s ∼M s ′ is the state’s indistinguishability relation w.r.t the model M. Then we say: Definition 1 (Con… view at source ↗
Figure 4
Figure 4. Figure 4: Organization of our approach for cryptographic protocols side-channel analysis. [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Running example. The assembly snippet corresponds to the highlighted [PITH_FULL_IMAGE:figures/full_fig_p005_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: A portion of BIR blocks of the BAC protocol illustrated in [PITH_FULL_IMAGE:figures/full_fig_p006_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Translating execution tree T to SAPIC+ model: e, x, x1, . . . , xn, y ∈ V are variables, n ∈ Npriv is a secret name, and not, equal, plus, mult, f ∈ F are function symbols. o s and conditional observations are either normal or shadow observations. During transpilation of binary code into BIR, we insert assertions that encode well-formedness invariants of execu￾tions, e.g., after each stack operation we add… view at source ↗
Figure 8
Figure 8. Figure 8: The observed access latency (∆t) during the designated time period. session builder represents the address of the function that initiates a secure session, while OTPK exists indicates the address of an instruction executed when a one-time pre-key is used in the creation of the master secret key for the secure session. [89] C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. van der Merwe, “A Comprehensive … view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper presents a toolchain that lifts selected regions of machine code from binaries to an IR, instruments the IR with explicit leakage contracts for constant-time and Spectre-PHT-style speculative observations, symbolically executes to obtain event/observation traces, and translates the traces into Sapic for analysis with Tamarin, ProVerif, and DeepSec. Case studies extract models of WhatsApp Desktop session-management and double-ratchet components to analyze forward secrecy and post-compromise security under state-cloning, and analyze the BAC protocol, reporting discovery of an instruction-cache side channel in WhatsApp enabling social-graph inference plus reproduction of known unlinkability issues in BAC.

Significance. If the lifting and contract fidelity hold, the work would meaningfully advance automated analysis of microarchitectural side channels in real cryptographic protocol binaries, bridging the gap between symbolic protocol models and deployed implementations. The WhatsApp and BAC case studies provide concrete demonstrations of both new leak discovery and reproduction of known issues under explicit observation models.

major comments (1)
  1. [Section 4 and Section 5] Section 4 (lifting and instrumentation) and Section 5 (case studies): the central claims that the extracted traces enable sound side-channel analysis of forward secrecy, post-compromise security, and the reported instruction-cache channel rest on the unvalidated assumption that the chosen lifting rules and leakage contracts neither fabricate nor omit microarchitectural observations that would occur on real hardware. No direct comparison of generated traces against hardware measurements (cache-timing, branch-predictor state, or standard side-channel benchmarks) on the same binaries is provided.
minor comments (1)
  1. [Abstract] The abstract states that known unlinkability issues in BAC are reproduced but does not cite the specific prior results being reproduced.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive review and for identifying an important aspect of our presentation. The major comment concerns the validation of lifting rules and leakage contracts. We respond to this point below and describe the revisions we will make to improve clarity around our modeling assumptions.

read point-by-point responses

  1. Referee: [Section 4 and Section 5] Section 4 (lifting and instrumentation) and Section 5 (case studies): the central claims that the extracted traces enable sound side-channel analysis of forward secrecy, post-compromise security, and the reported instruction-cache channel rest on the unvalidated assumption that the chosen lifting rules and leakage contracts neither fabricate nor omit microarchitectural observations that would occur on real hardware. No direct comparison of generated traces against hardware measurements (cache-timing, branch-predictor state, or standard side-channel benchmarks) on the same binaries is provided.

    Authors: We acknowledge that the manuscript does not contain direct empirical comparisons of the generated traces against hardware measurements on the analyzed binaries. Our central claims are conditioned on the explicit leakage contracts we instrument; the soundness of the subsequent symbolic analysis (forward secrecy, post-compromise security, and the reported instruction-cache channel) holds relative to those contracts rather than to an unstated claim of exact hardware fidelity. The contracts themselves are drawn from standard models in the constant-time and speculative-execution literature. To address the concern, we will revise Section 4 to add a subsection that (i) details the lifting rules and their correspondence to observable microarchitectural events and (ii) cites prior validation efforts on similar binary-lifting techniques. We will also insert a limitations paragraph in Section 5 that explicitly states the absence of hardware trace comparisons and discusses how discrepancies could arise. These changes will make the scope of our claims and the underlying assumptions transparent to readers. revision: partial

Circularity Check

0 steps flagged

No circularity: systems tooling paper with independent pipeline implementation

full rationale

This is a systems and tooling paper whose central contribution is an implemented pipeline for binary lifting to IR, leakage contract instrumentation, symbolic execution to traces, and export to Sapic/Tamarin/ProVerif/DeepSec. No equations, fitted parameters, or self-referential definitions appear in the described derivation chain. The analyses of WhatsApp components and BAC protocol follow directly from applying the toolchain to selected binary regions under explicitly chosen observation models; results are not forced by construction from the inputs. Concerns about hardware fidelity of the lifted IR and contracts are correctness risks, not circularity. The paper is self-contained against external benchmarks via case studies on real binaries.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that binary lifting and leakage contracts faithfully model hardware observations; no free parameters or new invented entities are introduced in the abstract.

axioms (1)
  • domain assumption The chosen intermediate representation and symbolic execution semantics preserve the leakage-relevant behavior of the original machine code.
    Invoked when the abstract states that machine code is lifted to an IR and instrumented with leakage contracts before symbolic execution.

pith-pipeline@v0.9.0 · 5496 in / 1403 out tokens · 47893 ms · 2026-05-17T22:09:30.407808+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

93 extracted references · 93 canonical work pages

  1. [1]

    This poodle bites: exploiting the ssl 3.0 fallback,

    M. Bodo, T. Duong, and K. Kotowicz, “This poodle bites: exploiting the ssl 3.0 fallback,” inSecurity Advisory 21, 2014, pp. 34–58

    work page 2014

  2. [2]

    Cryptobap: A binary analysis platform for cryptographic protocols,

    F. Nasrabadi, R. K ¨unnemann, and H. Nemati, “Cryptobap: A binary analysis platform for cryptographic protocols,” inProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS ’23), November 26–30, 2023, Copenhagen, Denmark, 2023, pp. 1362–1376. [Online]. Available: https://doi.org/10.1145/ 3576915.3623090

    work page arXiv 2023

  3. [3]

    Symbolic parallel composition for multi-language protocol verification,

    ——, “Symbolic parallel composition for multi-language protocol verification,”to appear in the 38th IEEE Computer Security Foundations Symposium (CSF), 2025. [Online]. Available: https: //arxiv.org/abs/2504.06833

    work page arXiv 2025

  4. [4]

    Binsec: Binary code analysis with low-level regions,

    A. Djoudi and S. Bardin, “Binsec: Binary code analysis with low-level regions,” inProceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume

    work page

  5. [5]

    Berlin, Heidelberg: Springer-Verlag, 2015, p. 212–217. [Online]. Available: https://doi.org/10.1007/978-3-662-46681-0 17

    work page doi:10.1007/978-3-662-46681-0 2015

  6. [6]

    BAP: A binary analysis platform,

    D. Brumley, I. Jager, T. Avgerinos, and E. J. Schwartz, “BAP: A binary analysis platform,” inComputer Aided Verification, 2011, pp. 463–469

    work page 2011

  7. [7]

    Val- idation of abstract side-channel models for computer architectures,

    H. Nemati, P. Buiras, A. Lindner, R. Guanciale, and S. Jacobs, “Val- idation of abstract side-channel models for computer architectures,” in Computer Aided Verification, S. K. Lahiri and C. Wang, Eds. Cham: Springer International Publishing, 2020, pp. 225–248

    work page 2020

  8. [8]

    Validation of side-channel models via observation refinement,

    P. Buiras, H. Nemati, A. Lindner, and R. Guanciale, “Validation of side-channel models via observation refinement,” inMICRO, 2021. [Online]. Available: https://doi.org/10.1145/3466752.3480130

    work page doi:10.1145/3466752.3480130 2021

  9. [9]

    Hardware-software contracts for secure speculation,

    M. Guarnieri, B. K ¨opf, J. Reineke, and P. Vila, “Hardware-software contracts for secure speculation,” in2021 IEEE Symposium on Security and Privacy (SP). IEEE, 2021, pp. 1868–1883

    work page 2021

  10. [10]

    Most Popular Messaging Apps In 2025

    “Most Popular Messaging Apps In 2025.” [Online]. Available: https: //www.similarweb.com/blog/research/apps/worldwide-messaging-apps/

    work page 2025

  11. [11]

    Formal Analysis of Session- Handling in Secure Messaging: Lifting Security from Sessions to Conversations,

    C. Cremers, C. Jacomme, and A. Naska, “Formal Analysis of Session- Handling in Secure Messaging: Lifting Security from Sessions to Conversations,” in32nd USENIX Security Symposium (USENIX Security 23), 2023, pp. 1235–1252. [Online]. Available: https://www.usenix.org/ conference/usenixsecurity23/presentation/cremers-session-handling

    work page 2023

  12. [12]

    Membership Inference Attacks From First Principles

    S. Cauligi, C. Disselkoen, D. Moghimi, G. Barthe, and D. Stefan, “Sok: Practical foundations for software spectre defenses,” in43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 2022, pp. 666–680. [Online]. Available: https://doi.org/10.1109/SP46214.2022.9833707

    work page doi:10.1109/sp46214.2022.9833707 2022

  13. [13]

    Trabin: Trustworthy analyses of binaries,

    A. Lindner, R. Guanciale, and R. Metere, “Trabin: Trustworthy analyses of binaries,”Sci. Comput. Program., vol. 174, pp. 72–89,

    work page

  14. [14]

    Available: https://doi.org/10.1016/j.scico.2019.01.001

    [Online]. Available: https://doi.org/10.1016/j.scico.2019.01.001

    work page doi:10.1016/j.scico.2019.01.001 2019

  15. [15]

    Hol interactive theorem prover,

    H. development team, “Hol interactive theorem prover,” 2022. [Online]. Available: https://hol-theorem-prover.org/

    work page 2022

  16. [16]

    L3: A Specification Language for Instruction Set Architectures

    A. Fox, “L3: A Specification Language for Instruction Set Architectures.” [Online]. Available: https://acjf3.github.io/l3

    work page

  17. [17]

    Proof-producing symbolic execution for binary code verification,

    A. Lindner, R. Guanciale, and M. Dam, “Proof-producing symbolic execution for binary code verification,” 2023. [Online]. Available: https://arxiv.org/abs/2304.08848

    work page arXiv 2023

  18. [18]

    Proving noninterference and functional correctness using traces

    J. McLean, “Proving noninterference and functional correctness using traces,”J. Comput. Secur., vol. 1, no. 1, pp. 37–58, 1992. [Online]. Available: https://doi.org/10.3233/JCS-1992-1103

    work page doi:10.3233/jcs-1992-1103 1992

  19. [19]

    On the security of public key protocols (extended abstract),

    D. Dolev and A. C. Yao, “On the security of public key protocols (extended abstract),” in22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981. IEEE Computer Society, 1981, pp. 350–357. [Online]. Available: https://doi.org/10.1109/SFCS.1981.32

    work page doi:10.1109/sfcs.1981.32 1981

  20. [20]

    The tamarin prover for the symbolic analysis of security protocols,

    S. Meier, B. Schmidt, C. Cremers, and D. Basin, “The tamarin prover for the symbolic analysis of security protocols,” inComputer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25. Springer, 2013, pp. 696–701

    work page 2013

  21. [21]

    An efficient cryptographic protocol verifier based on prolog rules

    B. Blanchetet al., “An efficient cryptographic protocol verifier based on prolog rules.” in14th IEEE Computer Security Foundations Workshop (CSFW-14), vol. 1, 2001, pp. 82–96

    work page 2001

  22. [22]

    Deepsec: deciding equiva- lence properties in security protocols theory and practice,

    V . Cheval, S. Kremer, and I. Rakotonirina, “Deepsec: deciding equiva- lence properties in security protocols theory and practice,” in2018 IEEE symposium on security and privacy (SP). IEEE, 2018, pp. 529–546

    work page 2018

  23. [23]

    Automated analysis of security protocols with global state,

    S. Kremer and R. K ¨unnemann, “Automated analysis of security protocols with global state,”Journal of Computer Security, vol. 24, no. 5, pp. 583– 616, 2016

    work page 2016

  24. [24]

    Cryptanalysis of DES implemented on computers with cache,

    Y . Tsunoo, T. Saito, T. Suzaki, and M. Shigeri, “Cryptanalysis of DES implemented on computers with cache,” inProceedings of the Workshop on Cryptographic Hardware and Embedded Systems, ser. CHES’03, LNCS. Springer, 2003, pp. 62–76

    work page 2003

  25. [25]

    Trace-driven Cache Attacks on AES (Short Paper),

    O. Acıic ¸mez and C ¸ . K. Koc ¸, “Trace-driven Cache Attacks on AES (Short Paper),” inProceedings of the 8th International Conference on Information and Communications Security, ser. ICICS. Springer-Verlag, 2006, pp. 112–121

    work page 2006

  26. [26]

    Advances on access-driven cache attacks on AES,

    M. Neve and J.-P. Seifert, “Advances on access-driven cache attacks on AES,” inProceedings of the 13th International Conference on Selected Areas in Cryptography, ser. SAC’06. Springer-Verlag, 2007, pp. 147– 162

    work page 2007

  27. [27]

    Efficient cache attacks on AES, and countermeasures,

    E. Tromer, D. A. Osvik, and A. Shamir, “Efficient cache attacks on AES, and countermeasures,”J. Cryptol., vol. 23, no. 2, pp. 37–71, Jan. 2010

    work page 2010

  28. [28]

    Cache Missing for Fun and Profit,

    C. Percival, “Cache Missing for Fun and Profit,” inBSDCan, 2005

    work page 2005

  29. [29]

    Inspectre: Breaking and fixing microarchitectural vulnerabilities by formal analysis,

    R. Guanciale, M. Balliu, and M. Dam, “Inspectre: Breaking and fixing microarchitectural vulnerabilities by formal analysis,” inProceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020, pp. 1853–1869. 14

    work page 2020

  30. [30]

    System- level non-interference for constant-time cryptography,

    G. Barthe, G. Betarte, J. Campo, C. Luna, and D. Pichardie, “System- level non-interference for constant-time cryptography,” inProceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014, pp. 1267–1279

    work page 2014

  31. [31]

    Daniel gruss, werner haas, mike hamburg, moritz lipp, stefan mangard, thomas prescher, michael schwarz, and yuval yarom. spectre attacks: Exploiting speculative exe- cution,

    P. Kocher, J. Horn, A. Fogh, and D. Genkin, “Daniel gruss, werner haas, mike hamburg, moritz lipp, stefan mangard, thomas prescher, michael schwarz, and yuval yarom. spectre attacks: Exploiting speculative exe- cution,” in40th IEEE Symposium on Security and Privacy (S&P’19), 2019

    work page 2019

  32. [32]

    Automated side-channel analysis of cryptographic protocol implementations-source code,

    F. Nasrabadi, R. K ¨unnemann, and H. Nemati, “Automated side-channel analysis of cryptographic protocol implementations-source code,” 2025. [Online]. Available: https://github.com/FMSecure/CryptoBAP

    work page 2025

  33. [33]

    David,Ghidra Software Reverse Engineering for Beginners: Analyze, identify, and avoid malicious code and potential threats in your networks and systems

    A. David,Ghidra Software Reverse Engineering for Beginners: Analyze, identify, and avoid malicious code and potential threats in your networks and systems. Packt Publishing Ltd, 2021

    work page 2021

  34. [34]

    Pki for machine readable travel documents offering icc read-only access,

    P. T. Force, “Pki for machine readable travel documents offering icc read-only access,”Technical report, International Civil Aviation Orga- nization, 2004

    work page 2004

  35. [35]

    Where’s crypto?: Automated identification and classification of proprietary cryptographic primitives in binary code,

    C. Meijer, V . Moonsamy, and J. Wetzels, “Where’s crypto?: Automated identification and classification of proprietary cryptographic primitives in binary code,” in30th USENIX Security Symposium (USENIX Security 21), 2021, pp. 555–572

    work page 2021

  36. [36]

    Val- idation of abstract side-channel models for computer architectures,

    H. Nemati, P. Buiras, A. Lindner, R. Guanciale, and S. Jacobs, “Val- idation of abstract side-channel models for computer architectures,” inComputer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I 32. Springer, 2020, pp. 225–248

    work page 2020

  37. [37]

    Klee: unassisted and automatic generation of high-coverage tests for complex systems programs

    C. Cadar, D. Dunbaret al., “Klee: unassisted and automatic generation of high-coverage tests for complex systems programs.”

    work page

  38. [38]

    A. V . Hoe, R. Sethi, and J. D. Ullman,Compilers-principles, techniques, and tools. Pearson Addison Wesley Longman Boston, 1986

    work page 1986

  39. [40]

    Inc., Tech

    S. Inc., Tech. Rep., Latest Version Updated on 2025. [Online]. Available: https://signal.org/docs/

    work page 2025

  40. [41]

    SAPIC+: Protocol verifiers of the world, unite!

    V . Cheval, C. Jacomme, S. Kremer, U. de Lorraine, I. Nancy, and R. K ¨unnemann, “SAPIC+: Protocol verifiers of the world, unite!”

    work page

  41. [42]

    An Algebra for Symbolic Diffie-Hellman Protocol Analysis,

    D. J. Dougherty and J. D. Guttman, “An Algebra for Symbolic Diffie-Hellman Protocol Analysis,” inTrustworthy Global Computing, D. Hutchison, T. Kanade, J. Kittler, J. M. Kleinberg, F. Mattern, J. C. Mitchell, M. Naor, O. Nierstrasz, C. Pandu Rangan, B. Steffen, M. Sudan, D. Terzopoulos, D. Tygar, M. Y . Vardi, G. Weikum, C. Palamidessi, and M. D. Ryan, Ed...

    work page doi:10.1007/978-3-642-41157-1 2013

  42. [43]

    Enumerable sets are diophantine,

    Y . Matiyaseviˇc, “Enumerable sets are diophantine,”Mathematical logic in the 20th century, pp. 269–273, 2003

    work page 2003

  43. [44]

    WhatsApp Encryption Overview,

    WhatsApp Inc. / Meta Platforms, “WhatsApp Encryption Overview,” Tech. Rep., Version 8 Updated August 19, 2024

    work page 2024

  44. [45]

    Practical eavesdropping and skimming attacks on high- frequency rfid tokens,

    G. P. Hancke, “Practical eavesdropping and skimming attacks on high- frequency rfid tokens,”Journal of Computer Security, vol. 19, no. 2, pp. 259–288, 2011

    work page 2011

  45. [46]

    A survey of security and privacy issues in epassport protocols,

    G. Avoine, A. Beaujeant, J. Hernandez-Castro, L. Demay, and P. Teuwen, “A survey of security and privacy issues in epassport protocols,”ACM Computing Surveys (CSUR), vol. 48, no. 3, pp. 1–37, 2016

    work page 2016

  46. [47]

    Analysing unlinka- bility and anonymity using the applied pi calculus,

    M. Arapinis, T. Chothia, E. Ritter, and M. Ryan, “Analysing unlinka- bility and anonymity using the applied pi calculus,” in2010 23rd IEEE computer security foundations symposium. IEEE, 2010, pp. 107–121

    work page 2010

  47. [48]

    A traceability attack against e-passports,

    T. Chothia and V . Smirnov, “A traceability attack against e-passports,” in International Conference on Financial Cryptography and Data Security. Springer, 2010, pp. 20–34

    work page 2010

  48. [49]

    DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice,

    V . Cheval, S. Kremer, and I. Rakotonirina, “DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice,” in2018 IEEE Symposium on Security and Privacy (SP). San Francisco, CA: IEEE, May 2018, pp. 529–546. [Online]. Available: https://ieeexplore.ieee.org/document/8418623/

    work page arXiv 2018

  49. [50]

    Putin launches spy app to keep russians in ‘digi- tal gulag’,

    M. Bennetts, “Putin launches spy app to keep russians in ‘digi- tal gulag’,” https://www.thetimes.com/world/russia-ukraine-war/article/ putin-moscow-whatsapp-ban-plan-max-app-launch-b789tt6ts

    work page

  50. [51]

    E-government,

    “E-government,” https://en.wikipedia.org/wiki/E-government

    work page

  51. [52]

    “Absher,” https://en.wikipedia.org/wiki/Absher %28application%29

    work page

  52. [53]

    Singpass singapore’s national digital identity (factsheet),

    “Singpass singapore’s national digital identity (factsheet),” https://www. mddi.gov.sg/newsroom/singpass-factsheet-02032022

    work page

  53. [54]

    E-government in europe,

    M. Bennetts, “E-government in europe,” https://en.wikipedia.org/wiki/ E-government in Europe

    work page

  54. [55]

    Electronic monitoring smartphone apps: An analysis of risks from technical, Human-Centered, and legal perspectives,

    K. Owens, A. Alem, F. Roesner, and T. Kohno, “Electronic monitoring smartphone apps: An analysis of risks from technical, Human-Centered, and legal perspectives,” in31st USENIX Security Symposium (USENIX Security 22). Boston, MA: USENIX Association, Aug. 2022, pp. 4077–4094. [Online]. Available: https://www.usenix.org/conference/ usenixsecurity22/presenta...

    work page 2022

  55. [56]

    Tracetogether,

    “Tracetogether,” https://en.wikipedia.org/wiki/TraceTogether

    work page

  56. [57]

    An attack on the Needham-Schroeder public- key authentication protocol,

    G. Lowe, “An attack on the Needham-Schroeder public- key authentication protocol,”Information Processing Letters, vol. 56, no. 3, pp. 131–133, Nov. 1995. [Online]. Available: https://linkinghub.elsevier.com/retrieve/pii/0020019095001442

    work page arXiv 1995

  57. [58]

    The inductive approach to verifying cryptographic protocols,

    L. C. Paulson, “The inductive approach to verifying cryptographic protocols,”Journal of Computer Security, vol. 6, no. 1-2, pp. 85–128, Jan. 1998. [Online]. Available: https://journals.sagepub.com/ action/showAbstract

    work page 1998

  58. [59]

    Abstract modeling of system communication in constructive cryptography using crypthol,

    D. Basin, A. Lochbihler, U. Maurer, and S. R. Sefidgar, “Abstract modeling of system communication in constructive cryptography using crypthol,” in2021 IEEE 34th Computer Security Foundations Sympo- sium (CSF). IEEE, 2021, pp. 1–16

    work page 2021

  59. [60]

    Model Checking Security Protocols,

    D. Basin, C. Cremers, and C. Meadows, “Model Checking Security Protocols,” inHandbook of Model Checking, E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Eds. Cham: Springer International Publishing, 2018, pp. 727–762. [Online]. Available: https://doi.org/10. 1007/978-3-319-10575-8 22

    work page 2018

  60. [61]

    The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm,

    B. Blanchet, “The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm,”Electronic Proceedings in Theoretical Computer Science, vol. 373, pp. 14–22, Nov. 2022. [Online]. Available: http://arxiv.org/abs/2211.12227v1

    work page arXiv 2022

  61. [62]

    The TAMARIN Prover for the Symbolic Analysis of Security Protocols,

    S. Meier, B. Schmidt, C. Cremers, and D. Basin, “The TAMARIN Prover for the Symbolic Analysis of Security Protocols,” inComputer Aided Verification, D. Hutchison, T. Kanade, J. Kittler, J. M. Kleinberg, F. Mattern, J. C. Mitchell, M. Naor, O. Nierstrasz, C. Pandu Rangan, B. Steffen, M. Sudan, D. Terzopoulos, D. Tygar, M. Y . Vardi, G. Weikum, N. Sharygina...

    work page doi:10.1007/978-3-642-39799-8 2013

  62. [63]

    Meltdown: Reading kernel memory from user space,

    M. Lipp, M. Schwarz, D. Gruss, T. Prescher, W. Haas, J. Horn, S. Mangard, P. Kocher, D. Genkin, Y . Yaromet al., “Meltdown: Reading kernel memory from user space,”Communications of the ACM, vol. 63, no. 6, pp. 46–56, 2020

    work page 2020

  63. [64]

    Spectre attacks: Exploit- ing speculative execution,

    P. Kocher, J. Horn, A. Fogh, D. Genkin, D. Gruss, W. Haas, M. Ham- burg, M. Lipp, S. Mangard, T. Prescheret al., “Spectre attacks: Exploit- ing speculative execution,”Communications of the ACM, vol. 63, no. 7, pp. 93–101, 2020

    work page 2020

  64. [65]

    Security flaws caused by compiler optimizations,

    H. Sidhpurwala, “Security flaws caused by compiler optimizations,”Red Hat Blog, 2019

    work page 2019

  65. [66]

    What you get is what you c: Controlling side effects in mainstream c compilers,

    L. Simon, D. Chisnall, and R. Anderson, “What you get is what you c: Controlling side effects in mainstream c compilers,” in2018 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 2018, pp. 1–15

    work page 2018

  66. [67]

    Coverage-based grey- box fuzzing as markov chain,

    M. B ¨ohme, V .-T. Pham, and A. Roychoudhury, “Coverage-based grey- box fuzzing as markov chain,” inProceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016, pp. 1032–1043

    work page 2016

  67. [68]

    Dy fuzzing: formal dolev- yao models meet cryptographic protocol fuzz testing,

    M. Ammann, L. Hirschi, and S. Kremer, “Dy fuzzing: formal dolev- yao models meet cryptographic protocol fuzz testing,” in2024 IEEE Symposium on Security and Privacy (SP). IEEE, 2024, pp. 1481–1499

    work page 2024

  68. [69]

    Differential testing for software,

    W. M. McKeeman, “Differential testing for software,”Digital Technical Journal, vol. 10, no. 1, pp. 100–107, 1998

    work page 1998

  69. [70]

    Verifying cryptographic security implementations in c using automated model extraction,

    M. Aizatulin, “Verifying cryptographic security implementations in c using automated model extraction,” Ph.D. dissertation, The Open University, 2015. [Online]. Available: http://arxiv.org/abs/2001.00806

    work page arXiv 2015

  70. [71]

    From computationally-proved protocol speci- fications to implementations,

    D. Cad ´e and B. Blanchet, “From computationally-proved protocol speci- fications to implementations,” in2012 Seventh International Conference on Availability, Reliability and Security. IEEE, 2012, pp. 65–74

    work page 2012

  71. [72]

    Secure Synthesis of Distributed Cryptographic Applications,

    C. Acay, J. Gancher, R. Recto, and A. C. Myers, “Secure Synthesis of Distributed Cryptographic Applications,” in2024 IEEE 37th Computer Security Foundations Symposium (CSF). IEEE Computer Society, Jul. 2024, pp. 433–448. [Online]. Available: https://www.computer.org/csdl/ proceedings-article/csf/2024/620300a315/1W0eVQN43Kw

    work page 2024

  72. [73]

    Verus: A Practical Foundation for Systems Verification,

    A. Lattuada, T. Hance, J. Bosamiya, M. Brun, C. Cho, H. LeBlanc, P. Srinivasan, R. Achermann, T. Chajed, C. Hawblitzel, J. Howell, J. R. Lorch, O. Padon, and B. Parno, “Verus: A Practical Foundation for Systems Verification,” inProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, ser. SOSP ’24. New York, NY , USA: Association for ...

    work page doi:10.1145/3694715.3695952 2024

  73. [74]

    Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version),

    L. Arquint, F. A. Wolf, J. Lallemand, R. Sasse, C. Sprenger, S. N. Wiesner, D. Basin, and P. M ¨uller, “Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version),” Dec. 2022. [Online]. Available: http://arxiv.org/abs/2212. 04171

    work page 2022

  74. [75]

    Modular verification of security protocol code by typing,

    K. Bhargavan, C. Fournet, and A. D. Gordon, “Modular verification of security protocol code by typing,”ACM Sigplan Notices, vol. 45, no. 1, pp. 445–456, 2010

    work page 2010

  75. [76]

    miTLS: Verifying protocol implementations against real-world attacks,

    K. Bhargavan, C. Fournet, and M. Kohlweiss, “miTLS: Verifying protocol implementations against real-world attacks,”IEEE Security & Privacy, vol. 14, no. 6, pp. 18–25, 2016. [Online]. Available: https://doi.org/10.1109/MSP.2016.123

    work page doi:10.1109/msp.2016.123 2016

  76. [77]

    Verified reference implementations of ws-security protocols,

    K. Bhargavan, C. Fournet, and A. D. Gordon, “Verified reference implementations of ws-security protocols,” inInternational Workshop on Web Services and Formal Methods. Springer, 2006, pp. 88–106

    work page 2006

  77. [78]

    Computationally sound verifi- cation of source code,

    M. Backes, M. Maffei, and D. Unruh, “Computationally sound verifi- cation of source code,” inProceedings of the 17th ACM conference on Computer and communications security, 2010, pp. 387–398

    work page 2010

  78. [79]

    Verified models and reference implementations for the tls 1.3 standard candidate,

    K. Bhargavan, B. Blanchet, and N. Kobeissi, “Verified models and reference implementations for the tls 1.3 standard candidate,” in2017 IEEE Symposium on Security and Privacy (SP). IEEE, 2017, pp. 483– 502

    work page 2017

  79. [80]

    Using elyjah to analyse java implementations of cryp- tographic protocols,

    N. O’Shea, “Using elyjah to analyse java implementations of cryp- tographic protocols,” inJoint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS-2008), 2008

    work page 2008

  80. [81]

    Automated security verification for crypto protocol imple- mentations: Verifying the jessie project,

    J. J ¨urjens, “Automated security verification for crypto protocol imple- mentations: Verifying the jessie project,”Electronic Notes in Theoretical Computer Science, vol. 250, no. 1, pp. 123–136, 2009

    work page 2009

Showing first 80 references.