Pith. sign in

REVIEW 4 major objections 5 minor 71 references

Beyond the Quantum Promise: A Security Analysis of Classical Control in Quantum Key Distribution

T0 review · 4 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper claims that quantum key distribution as standardized by ETSI and ITU-T is vulnerable to three specification-level attacks that break key secrecy or authentication, and that two protocol changes restore the checked properties in…

desk verdict A reproducible Tamarin artifact and two plausible control-plane findings, but the EB attack's undetectability claim contradicts the CHSH statistics and V1 does not hold as stated. read the letter →

arxiv 2608.07626 v1 pith:AH4ORTU3 submitted 2026-08-07 quant-ph cs.CRcs.SC

Ali Hamza Malik , Raja Hasnain Anwar , Muhammad Taqi Raza This is my paper · ORCID
classification quant-phcs.CRcs.SC MSC 81P9468Q6094A60 PACS 03.67.Dd
keywords quantumkeydistributionsymbolicverificationTamarinproverclassicalcontrolplaneentanglement-basedQKDprepare-and-measuremessageauthenticationcodesETSIandITU-Tstandards
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Quantum key distribution's security claims rest on the correct interplay between its quantum phase and its classical control plane, yet the ETSI and ITU-T standardization documents that govern QKD leave ordering, timing, and message-binding details underspecified. The paper builds a symbolic model of both prepare-and-measure and entanglement-based QKD protocols, grounded in those standards, and verifies it with an automated prover under a combined quantum-classical adversary. It reports three specification-level vulnerability classes—subverted entanglement injection, basis-deferred measurement, and message reflection—that break session-key secrecy or entity authentication in the model. It then shows that adding a measurement-commitment phase and identity-bound message authentication codes restores all checked properties across nine protocol configurations. The claim is deliberately scoped to the symbolic abstraction: it identifies structural omissions in the standards, not vendor-specific or coherence-based attacks.

What carries the argument

The carrying object is a family of symbolic QKD protocol models written for the Tamarin Prover and generated from a single m4 template: quantum operations are represented as uninterpreted symbolic functions with logical conditions (for example, Bob's detection check $\mathit{check}(s_A,s_B)$), so that the causal dependency between quantum measurement outcomes and classical post-processing messages is preserved without modeling probabilities. The adversary Eve+ is a parallel composition of the quantum eavesdropper Eve and a classical Dolev-Yao network adversary, encoded as non-deterministic transitions over unidirectional quantum and classical channels, with linear (non-persistent) states to enforce the no-cloning restriction. Security goals are stated as Tamarin lemmas: session-key secrecy, executability, and Lowe's non-injective agreement, with failures examined through counterexample traces.

What would settle it

Re-run the V1 attack as described (Eve keeps one branch, measures after Bob's basis announcement, re-encodes a stream for Alice) in a circuit simulator that computes the CHSH parameter S over all four basis-pair combinations and applies a 10% relative-error threshold; if S is near 0 rather than near -2.82, the paper's Figure 7(b) does not represent the attack and the undetectability claim collapses. Equivalently, inspect the QVerify Tamarin model's check() function to confirm it omits the CHSH statistic, which would mean the V1 counterexample was found by a model that never tests the very statistic the honest protocol uses to detect tampering.

Watch

Extended reading notes

Core claim

Under an adversary that combines the capabilities of a quantum eavesdropper and a classical network attacker (Eve+), the paper finds that the procedure texts of ETSI and ITU-T QKD specifications omit constraints that are security-critical in the symbolic model. In entanglement-based QKD, an attacker who controls the source and the clock can inject a time shift, read one party's basis announcement, measure the retained half of each entangled pair, and re-encode a matching stream for the other party, recovering the final key while the honest parties' parameter estimation accepts the session. In prepare-and-measure QKD, if Alice's basis announcement is permitted before Bob measures, an attacker can store intercepted qubits, measure them in the announced basis, and forward re-encoded qubits without increasing the detected error. In both families, MAC-authenticated classical messages that lack sender, receiver, and session-role binding can be reflected back to their originator, so a party accepts its own message as coming from the peer and agrees on a key derived from self-reflected data. The paper proposes a measurement-commitment phase and identity-bound MACs, and reports that Tamarin verification confirms these close all three vulnerabilities across nine protocol configurations without changing the quantum subroutines.

Load-bearing premise

The load-bearing premise is that the CHSH test accepts Eve's forged qubit stream, a claim the paper's simulation asserts but its symbolic model never actually tests, since the modeled detection check omits CHSH and the re-encoded stream may destroy mismatched-basis correlations.

Editorial extensions

If this is right

  • Standardization bodies would need to add explicit sequencing constraints, such as requiring both parties to commit to measurements before announcing bases, to close the timing window that enables V1 and V2.
  • MAC-based authentication of QKD classical messages would have to include sender and receiver identities, role metadata, and session context, preventing reflection and cross-session reuse.
  • Implementers who follow an announce-basis-before-measurement ordering would be operating outside the security guarantees of the standard, since the symbolic model falsifies key secrecy for that configuration.
  • Security proofs for QKD that assume an ideal classical infrastructure would not cover these control-plane failures, so protocol-level verification of the classical phase is needed in addition to information-theoretic quantum proofs.
  • The proposed countermeasures preserve the quantum subroutines, so they can be added without changing the optical hardware or encoding.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The V1 undetectability claim deserves scrutiny: the paper's simulation compares a noiseless attack circuit against a noisy honest baseline, but the attack as described destroys mismatched-basis CHSH correlations, so a faithful simulation may produce an S value near 0 that a 10% threshold would flag; the symbolic model omits CHSH from its detection check, so this falsification may be an artifact of
  • The same control-plane omissions likely extend beyond QKD to other quantum network protocols, such as entanglement distribution for repeaters and blind quantum computing, where timing and identity binding of classical control messages are equally underspecified.
  • A direct testable extension is to instantiate the full V1 attack in a quantum circuit simulator with honest CHSH parameter estimation and check whether the session survives; if it aborts, the claimed attack needs an explicit way to forge the Bell correlations.
  • If the fixes are adopted, the verification result suggests that QKD security statements should be expressed as hybrid properties covering both the quantum error test and the classical control-plane constraints, rather than as quantum-only guarantees.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper presents a Tamarin-based symbolic verification framework for QKD protocols grounded in ETSI and ITU-T specifications. It models both prepare-and-measure (PM) and entanglement-based (EB) variants under a combined quantum-classical Dolev-Yao adversary Eve+, and reports three specification-level vulnerabilities: subverted entanglement injection (V1), basis-deferred measurement (V2), and message reflection (V3). It proposes two countermeasures, measurement commitment (CM1) and identity-bound MACs (CM2), and verifies via Tamarin that these restore the checked secrecy and agreement lemmas across nine configurations. The QVerify artifact is publicly available and includes Tamarin models, m4 templates, and verification scripts.

Significance. The framework is a novel contribution: a unified, executable symbolic model of PM and EB QKD with authenticated classical channels and an adversary that controls both quantum and classical planes. The use of m4 templates to instantiate nine configurations and the public release of the toolchain are strengths. If the findings hold, the paper would be the first to demonstrate via automated verification that specification-level ordering and binding omissions in ETSI/ITU-T texts are security-critical. V2 (basis-deferred measurement) and V3 (message reflection) are well-grounded in the symbolic analysis and plausible as real specification gaps. The countermeasures are simple, protocol-level, and verified in the model. However, the overall significance is reduced by the serious internal inconsistency in the V1 analysis described in the major comments.

major comments (4)
  1. [§IV-A, §IV-D, Fig. 7(b)] The claim that the V1 attack is statistically indistinguishable from honest EB operation is inconsistent with the attack procedure. After Eve measures her retained qubit in Bob's announced basis b_B and re-encodes q'_A as an eigenstate of b_B, Alice's outcomes for any mismatched basis are random and independent of Bob's outcome. The CHSH correlator for mismatched settings is therefore 0, giving noiseless S = ±2 rather than S_ideal = -2√2, a relative error of about 29%, well above the 10% threshold marked in Figure 7. The simulated histograms in Figure 7(b) cannot arise from the described attack; either the circuits do not implement the described procedure or the statistical aggregation is erroneous. This contradiction undermines the central claim that CHSH-based parameter estimation would not flag the compromised session.
  2. [§III-A2, check(s_A, s_B)] The symbolic parameter-estimation check contains no Bell/CHSH term; it only verifies matched-basis consistency (q_x = q_A) and classical basis/bit agreement. The Tamarin falsification of Lemma 1 for the EB model under V1 is therefore an artifact of omitting the very test that is supposed to detect unentangled or re-encoded sources. The paper's own limitation statement ("established under a symbolic abstraction") does not remedy this, because §IV-D explicitly claims quantum-level evidence via Qiskit that is contradictory. The authors should either add a symbolic CHSH check and re-run the analysis, or explicitly restrict V1 to configurations without any Bell test and justify that restriction against the standards they cite.
  3. [§IV-A, Root Cause] The attack is described as a classical timing and synchronization omission, but the exploit mechanism is the re-encoding of qubits in Bob's announced basis. A protocol performing a CHSH test, as described in §II-D, would detect the re-encode regardless of any clock offset. Thus V1 is not a classical control-plane vulnerability in the same category as V2 and V3; it is a standard intercept-resend attack on entanglement-based QKD that the Bell test is designed to catch. This discrepancy should be addressed explicitly, and the Table I(a) row attributed to V1 (EB TWEC) should be re-evaluated.
  4. [§V-B] The countermeasure verification reuses the same abstraction, so the reported restoration of Lemma 1 for the previously V1-failing EB model does not confirm that CM1 defends against the physical V1 attack; it only confirms that the symbolic model without a Bell check becomes safe. The authors should decouple CM1's effect on V2 from its claimed effect on V1.
minor comments (5)
  1. [Fig. 7] The x-axis labels in both panels are non-uniform and do not match the stated 5% binning; the tick labels appear to skip values, making the histograms difficult to interpret. Please redraw the figures with consistent bins and labeled ticks.
  2. [Table I] The table formatting is ambiguous: the columns are not clearly separated, and the superscripts mapping falsifications to vulnerabilities are not explained in the caption. A dedicated legend or footnote defining V1, V2, V3 and the column semantics would improve readability.
  3. [§III-A2] The notation q_x and q_A is used for Bob's measured qubit and Alice's prepared qubit, respectively, but the protocol exchanges multiple qubits; please define the indexing or session context more precisely.
  4. [§IV-D] The simulation compares noiseless attack circuits against a noisy honest baseline. This asymmetry is of limited evidentiary value even apart from the S-value inconsistency, since any small structural deviation in the attack circuits would be masked by the honest baseline's noise. Please use identical noise models or justify the asymmetry.
  5. [Abstract] The abstract contains the typo "ahybridprotocol" in the first paragraph; please correct it.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: all claimed results are derived from explicit symbolic models and independently validated; the only self-link is to the public QVerify artifact and is not load-bearing.

full rationale

The paper's derivation chain is not circular. The Tamarin models are constructed explicitly from ETSI/ITU-T procedure texts, and the three vulnerability classes are consequences of concrete rewrite rules and lemmas; no parameter is fitted to the outcome and no target result is assumed in the model equations. The check(s_A, s_B) := (q_x = q_A) ∧ s_A = f(...) predicate is a deliberate symbolic abstraction of parameter estimation, and the V1/V2 attacks succeed in the model precisely because the attacker re-encodes qubits satisfying that predicate. This is the attack construction, not a hidden equivalence: the model transparently scopes out CHSH, noise, and coherent attacks, and the paper separately provides a Qiskit-based physical compatibility check that is not an input to the Tamarin analysis. Even if that Qiskit comparison is disputed, that is a correctness or modeling-scope concern, not circularity. The countermeasures CM1 and CM2 are independently re-verified in the same framework, and their success is a meaningful theorem about the strengthened models rather than a restatement of the fixes. The only self-reference is the QVerify artifact repository [26], which is a software release and does not carry the security argument. Thus no load-bearing step reduces by definition to its own inputs.

Assumptions & free parameters 2 free parameters · 5 assumptions · 0 invented entities

The central claims rest on the symbolic abstraction of quantum operations, the omission of CHSH from the EB parameter-estimation check, and the assumption that timing shifts are not detected. The Tamarin model has no fitted parameters; the Qiskit simulation introduces hand-chosen noise settings and a threshold. No new physical entities are introduced; Eve+ is a composed threat model (Eve parallel to AdvC), not a postulated physical object.

free parameters (2)
  • Qiskit Aer noise parameters = single-qubit gate error 0.0012, CX error 0.006, readout error 0.008
    Section IV-D. Hand-chosen baseline noise for the honest EB protocol; the V1 detectability comparison depends on this configuration.
  • CHSH acceptance threshold = 10% relative error
    Section IV-D, Figure 7. Hand-chosen threshold for flagging attacks; no derivation or justification is provided for this value.
assumptions (5)
  • domain assumption Quantum operations can be abstracted as uninterpreted symbolic functions without losing security-relevant ordering and dependency properties.
    Section III-A2. The model replaces probabilities with symbolic functions; coherent and superposition attacks are out of scope, so the proof only covers the modeled abstraction.
  • domain assumption Perfect MACs, ideal cryptographic primitives, and PSK pre-sharing.
    Sections II-A and III-B. Standard Dolev-Yao abstraction; PSKs are assumed to be delivered securely.
  • ad hoc to paper Eve+ can delay qubits and introduce clock offsets between Alice and Bob without detection.
    Section IV-A. Required for V1; the paper argues synchronization relies on NTP/analog sync, which are known vulnerable, but gives no physical-layer bound that prevents arbitrary delay in the model.
  • ad hoc to paper The symbolic parameter-estimation check is captured by check(s_A, s_B) on matched-basis consistency, omitting CHSH over mismatched bases.
    Sections III-A2 and IV-D. If a proper CHSH test is added, the V1 attack (S near 0) is detectable, so this is the key abstraction that produces the V1 result.
  • domain assumption Single-session model is sufficient for the security claims.
    Sections III-A1 and VI-A. Multi-session key management is deferred; the paper notes this boundary.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Beyond the Quantum Promise: A Security Analysis of Classical Control in Quantum Key Distribution." pith.science (2026). https://pith.science/paper/AH4ORTU3

@misc{pith2026260807626,
  author       = {Pith},
  title        = {Pith review of: Beyond the Quantum Promise: A Security Analysis of Classical Control in Quantum Key Distribution},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AH4ORTU3}},
  note         = {Machine review of arXiv:2608.07626}
}
read the original abstract

Quantum Key Distribution (QKD) protocols provide information-theoretic security by using quantum mechanical principles. Yet QKD is fundamentally a hybrid protocol: its security depends on the correct integration of the quantum phase with classical post-processing. While ETSI and ITUT specifications standardize QKD architectures and interfaces, they evaluate protocol security in isolation, leaving cross-layer interactions as an underexplored attack surface. This paper introduces a formal verification framework that holistically models QKD protocols based on ETSI and ITUT QKD specifications. Our model is the first hybrid QKD protocol model that supports automated analysis of protocollevel security focusing on how classical operations influence the security guarantees provided by the quantum phase of the QKD protocol. We formalize a comprehensive symbolic model of QKD protocols, based on ETSI and ITU-T QKD specifications, in Tamarin, an automated protocol verifier. Applying this framework, we obtain formal evidence of three specification-level vulnerabilities in ETSI- and ITU-T-grounded protocol models under adversary Eve+: subverted entanglement injection, basis-deferred measurement, and message reflection. Each arises from a classical control-plane omission in the procedure text and is established under a symbolic abstraction rather than as a claim about all practical deployments. We introduce two protocol improvements: measurement commitment and identitybound message authentication codes (MACs). Tamarin verification confirms that these countermeasures eliminate the identified vulnerabilities under Eve+. We have communicated our results and recommendations to relevant standardization organizations.

Figures

Figures reproduced from arXiv: 2608.07626 by the authors.

Figure 1
Figure 1. A typical two-node QKD architecture: (1*) shows a one-way quantum channel from Alice to Bob for PM QKD. (2a* and 2b*) depict quantum channels from a shared source of entangled qubit pairs to Alice and Bob for EB QKD. The control signals illustrate the interaction between quantum and classical phases. received comparatively less formal scrutiny as an integrated attack surface. Error-correction analyses [8], [16] typi… view at source ↗
Figure 2
Figure 2. Overview of a typical QKD protocol. Alice and Bob exchange [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. Overview of our methodology. as temporal logic lemmas over traces of rule actions. Tamarin supports automated and interactive proof search, and has been used to verify protocols including TLS 1.3 [43], 5G-AKA [44], EMV [45], Signal [46], and iMessage PQ3 [47]–[49]. III. DESIGN AND ANALYSIS OF FORMAL QKD MODEL We build an abstract QKD model, grounded in ITU and ETSI procedures (Appendix A), that ties classical messag… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Subverted Entanglement Injection attack. [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Basis-Deferred Measurement attack. Eve+ intercepts and stores Alice’s qubit stream, then measures it using Alice’s publicly revealed basis. She reconstructs and forwards a forged qubit sequence to Bob. With basis forwarding, Eve+ learns the final key without introducin…
Figure 6
Figure 6. Figure 6: Self-Authentication via Message Reflection. [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]
Figure 7
Figure 7. Figure 7: Relative CHSH violation error for adversarial and honest [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

71 extracted references · 61 canonical work pages

  1. [1]

    The evolution of quantum key distribution networks: On the road to the qinternet,

    Y . Cao, Y . Zhao, Q. Wang, J. Zhang, S. X. Ng, and L. Hanzo, “The evolution of quantum key distribution networks: On the road to the qinternet,”IEEE Communications Surveys & Tutorials, vol. 24, no. 2, pp. 839–894, 2022

    2022

  2. [2]

    Quantum key distribution: a networking perspective,

    M. Mehic, M. Niemiec, S. Rass, J. Ma, M. Peev, A. Aguado, V . Martin, S. Schauer, A. Poppe, C. Pacheret al., “Quantum key distribution: a networking perspective,”ACM Computing Surveys (CSUR), vol. 53, no. 5, pp. 1–41, 2020

    2020

  3. [3]

    Quantum cryptography in 5g networks: a comprehensive overview,

    M. Mehic, L. Michalek, E. Dervisevic, P. Burdiak, M. Plakalovic, J. Rozhon, N. Mahovac, F. Richter, E. Kaljic, F. Lauterbachet al., “Quantum cryptography in 5g networks: a comprehensive overview,” IEEE Communications Surveys & Tutorials, 2023

    work page 2023

  4. [4]

    Advances in quantum cryptography,

    S. Pirandola, U. L. Andersen, L. Banchi, M. Berta, D. Bunandar, R. Colbeck, D. Englund, T. Gehring, C. Lupo, C. Ottaviani, J. L. Pereira, M. Razavi, J. Shamsul Shaari, M. Tomamichel, V . C. Usenko, G. Vallone, P. Villoresi, and P. Wallden, “Advances in quantum cryptography,”Advances in Optics and Photonics, vol. 12, no. 4, p. 1012, Dec. 2020. [Online]. Av...

    doi:10.1364/aop.361502 2020

  5. [5]

    Architectural Principles for a Quantum Internet,

    W. Kozlowski, S. Wehner, R. V . Meter, B. Rijsman, A. S. Cacciapuoti, M. Caleffi, and S. Nagayama, “Architectural Principles for a Quantum Internet,” Internet Research Task Force (IRTF), Informational RFC 9340, Mar. 2023. [Online]. Available: https://www.rfc-editor.org/info/rfc9340

    work page 2023

  6. [6]

    Simple proof of security of the bb84 quantum key distribution protocol,

    P. W. Shor and J. Preskill, “Simple proof of security of the bb84 quantum key distribution protocol,”Physical review letters, vol. 85, no. 2, p. 441, 2000

    work page 2000

  7. [7]

    Cryptographic security of quantum key distribution,

    C. Portmann and R. Renner, “Cryptographic security of quantum key distribution,” 2014. [Online]. Available: https://arxiv.org/abs/1409.3525

    arXiv 2014

  8. [8]

    A largely self-contained and complete security proof for quantum key distribution,

    M. Tomamichel and A. Leverrier, “A largely self-contained and complete security proof for quantum key distribution,”Quantum, vol. 1, p. 14, 2017

    work page 2017

Show all 71 references
  1. [9]

    Quantum cryptogra- phy,

    N. Gisin, G. Ribordy, W. Tittel, and H. Zbinden, “Quantum cryptogra- phy,”Reviews of modern physics, vol. 74, no. 1, p. 145, 2002. [10]Quantum Key Distribution (QKD); Security Proofs, ETSI Std. ETSI GS QKD 005 V1.1.1, Dec. 2010. [Online]. Avail- able: https://www.etsi.org/deli...

    2002

  2. [11]

    Quantum copying: Beyond the no-cloning theorem,

    V . Bu ˇzek and M. Hillery, “Quantum copying: Beyond the no-cloning theorem,”Physical Review A, vol. 54, no. 3, p. 1844, 1996

    1996

  3. [12]

    Quantum uncertainty principles for measurements with interventions,

    Y . Xiao, Y . Yang, X. Wang, Q. Liu, and M. Gu, “Quantum uncertainty principles for measurements with interventions,”Physical Review Let- ters, vol. 130, no. 24, p. 240201, 2023

    2023

  4. [13]

    Evaluation of quantum key distribution systems against injection- locking attacks,

    J. Wiesemann, F. Gr ¨unenfelder, A. Bl´azquez, N. Walenta, and D. Rusca, “Evaluation of quantum key distribution systems against injection- locking attacks,”arXiv preprint arXiv:2412.10290, 2024

    2024 arXiv

  5. [14]

    Quantum key distribution with imperfectly isolated devices,

    X. Sixto, ´A. Navarrete, M. Pereira, G. Curr ´as-Lorenzo, K. Tamaki, and M. Curty, “Quantum key distribution with imperfectly isolated devices,” arXiv preprint arXiv:2411.13948, 2024

    2024 arXiv

  6. [15]

    Auto- matically identifying imperfections and attacks in practical quantum key distribution systems via machine learning,

    J. Xu, X. Ma, J. Liu, C. Zhang, H. Li, X. Zhou, and Q. Wang, “Auto- matically identifying imperfections and attacks in practical quantum key distribution systems via machine learning,”Science China Information Sciences, vol. 67, no. 10, p. 202501, 2024

    2024

  7. [16]

    Sifting attacks in finite-size quantum key distribution,

    C. Pfister, N. L ¨utkenhaus, S. Wehner, and P. J. Coles, “Sifting attacks in finite-size quantum key distribution,”New Journal of Physics, vol. 18, no. 5, p. 053001, 2016

    2016

  8. [17]

    Modelling and analysis of quantum key distribution protocols, bb84 and b92, in communicating quantum processes (cqp) language and analysing in prism,

    S. Kuppam, “Modelling and analysis of quantum key distribution protocols, bb84 and b92, in communicating quantum processes (cqp) language and analysing in prism,”arXiv preprint arXiv:1612.03706, 2016

    2016 arXiv

  9. [18]

    An automated analysis of the security of quantum key distribution,

    R. Nagarajan, N. Papanikolaou, G. Bowen, and S. Gay, “An automated analysis of the security of quantum key distribution,”arXiv preprint cs/0502048, 2005

    2005 arXiv

  10. [19]

    Formal verification of quantum protocols,

    R. Nagarajan and S. Gay, “Formal verification of quantum protocols,” arXiv preprint quant-ph/0203086, 2002

    2002 arXiv

  11. [20]

    Formal verification of the security of a free-space quantum key distribution system,

    V . Fern ´andez, M.-J. Garc ´ıa-Mart´ınez, L. Hern ´andez-Encinas, and A. Marti´ın, “Formal verification of the security of a free-space quantum key distribution system,” inProc. World Congr. Comput. Sci. Comput. Eng. Appl. Comput.(WORLDCOMP) Int. Conf. Security Manag.(SAM), 2011

    2011

  12. [21]

    A formal approach to unconditional security proofs for quantum key distribution,

    T. Kubota, Y . Kakutani, G. Kato, and Y . Kawano, “A formal approach to unconditional security proofs for quantum key distribution,” in Unconventional Computation: 10th International Conference, UC 2011, Turku, Finland, June 6-10, 2011. Proceedings 10. Springer, 2011, pp. 125–137

    2011

  13. [22]

    Model-checking quantum systems,

    M. Ying and Y . Feng, “Model-checking quantum systems,”National Science Review, vol. 6, no. 1, pp. 28–31, 2019

    2019

  14. [23]

    Symbolic abstractions for quantum protocol verification,

    L. Hirschi, D. Unruh, and M. Backes, “Symbolic abstractions for quantum protocol verification,” in2019 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 2019, pp. 1–16

    2019

  15. [24]

    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

    2013

  16. [25]

    Tamarin: verification of large-scale, real-world, cryptographic protocols,

    D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Tamarin: verification of large-scale, real-world, cryptographic protocols,”IEEE Security & Privacy, vol. 20, no. 3, pp. 24–32, 2022

    2022

  17. [26]

    QVerify,

    A. H. Malik, “QVerify,” https://github.com/KhwarizmiLab/QVerify, 2025, paper artifact for reproducing paper

    2025

  18. [27]

    Quantum key distribution with post-processing driven by physical unclonable functions,

    G. M. Nikolopoulos and M. Fischlin, “Quantum key distribution with post-processing driven by physical unclonable functions,”Applied Sci- ences, vol. 14, no. 1, p. 464, 2024

    2024

  19. [28]

    Experimental authentication of quantum key distribution with post-quantum cryptography,

    L.-J. Wang, K.-Y . Zhang, J.-Y . Wang, J. Cheng, Y .-H. Yang, S.-B. Tang, D. Yan, Y .-L. Tang, Z. Liu, Y . Yuet al., “Experimental authentication of quantum key distribution with post-quantum cryptography,”npj quantum information, vol. 7, no. 1, p. 67, 2021

    2021

  20. [29]

    Quantum cryptography: Public key distribution and coin tossing,

    C. H. Bennett and G. Brassard, “Quantum cryptography: Public key distribution and coin tossing,”Theoretical computer science, vol. 560, pp. 7–11, 2014

    2014

  21. [30]

    Quantum cryptography based on bell’s theorem,

    A. K. Ekert, “Quantum cryptography based on bell’s theorem,”Physical Review Letters, vol. 67, no. 6, p. 661, 1991

    1991

  22. [31]

    Realistic and general model for quantum key distribution with entangled-photon sources,

    Z.-Q. Zhong, S. Wang, X.-H. Zhan, Z.-Q. Yin, W. Chen, G.-C. Guo, and Z.-F. Han, “Realistic and general model for quantum key distribution with entangled-photon sources,”Physical Review A, vol. 106, no. 5, p. 052606, 2022

    2022

  23. [32]

    Experi- mental entanglement generation for quantum key distribution beyond 1 gbit/s,

    S. P. Neumann, M. Selimovic, M. Bohmann, and R. Ursin, “Experi- mental entanglement generation for quantum key distribution beyond 1 gbit/s,”Quantum, vol. 6, p. 822, 2022

    2022

  24. [33]

    Asymptotically optimal prepare-measure quantum key distri- bution protocol,

    H. Shu, “Asymptotically optimal prepare-measure quantum key distri- bution protocol,”International Journal of Theoretical Physics, vol. 62, no. 8, p. 191, 2023

    2023

  25. [34]

    Implementation of polarization- coded free-space bb84 quantum key distribution,

    Y . S. Kim, Y . C. Jeong, and Y . H. Kim, “Implementation of polarization- coded free-space bb84 quantum key distribution,”Laser Physics, vol. 18, pp. 810–814, 2008

    2008

  26. [35]

    Quantum key agreement protocol based on bb84,

    S.-K. Chong and T. Hwang, “Quantum key agreement protocol based on bb84,”Optics Communications, vol. 283, no. 6, pp. 1192–1195, 2010

    2010

  27. [36]

    Quantum key distribution network protocols: Quantum layer,

    H. Qin, P. Huang, and H. Wu, “Quantum key distribution network protocols: Quantum layer,” ITU-T Focus Group on Quantum Information Technology for Networks (FG QIT4N), Tech. Rep. Technical Report FG QIT4N D2.3.1, Nov

  28. [37]

    Continuous-variable quantum key distribution with entanglement in the middle,

    C. Weedbrook, “Continuous-variable quantum key distribution with entanglement in the middle,”Physical Review A—Atomic, Molecular, and Optical Physics, vol. 87, no. 2, p. 022308, 2013

    2013

  29. [38]

    Per- formance improvement of continuous-variable quantum key distribution with an entangled source in the middle via photon subtraction,

    Y . Guo, Q. Liao, Y . Wang, D. Huang, P. Huang, and G. Zeng, “Per- formance improvement of continuous-variable quantum key distribution with an entangled source in the middle via photon subtraction,”Physical Review A, vol. 95, no. 3, p. 032304, 2017

    2017

  30. [39]

    Proposed ex- periment to test local hidden-variable theories,

    J. F. Clauser, M. A. Horne, A. Shimony, and R. A. Holt, “Proposed ex- periment to test local hidden-variable theories,”Physical review letters, vol. 23, no. 15, p. 880, 1969

    1969

  31. [40]

    On the security of public key protocols,

    D. Dolev and A. Yao, “On the security of public key protocols,”IEEE Transactions on information theory, vol. 29, no. 2, pp. 198–208, 1983

    1983

  32. [41]

    Stallings,Network and internetwork security: principles and practice

    W. Stallings,Network and internetwork security: principles and practice. Prentice-Hall, Inc., 1995

    1995

  33. [42]

    The dolev-yao intruder is the most powerful attacker,

    I. Cervesato, “The dolev-yao intruder is the most powerful attacker,” inProceedings of the First International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security (MMM’01). Springer, 2001, pp. 159–176

    2001

  34. [43]

    A comprehensive symbolic analysis of tls 1.3,

    C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. Van Der Merwe, “A comprehensive symbolic analysis of tls 1.3,” inProceedings of the 2017 ACM SIGSAC conference on computer and communications security, 2017, pp. 1773–1788

    2017

  35. [44]

    A formal analysis of 5g authentication,

    D. Basin, J. Dreier, L. Hirschi, S. Radomirovic, R. Sasse, and V . Stettler, “A formal analysis of 5g authentication,” inProceedings of the 2018 ACM SIGSAC conference on computer and communications security, 2018, pp. 1383–1396

    2018

  36. [45]

    The emv standard: Break, fix, verify,

    D. Basin, R. Sasse, and J. Toro-Pozo, “The emv standard: Break, fix, verify,” in2021 IEEE Symposium on Security and Privacy (SP). IEEE, 2021, pp. 1766–1781

    2021

  37. [46]

    A formal security analysis of the signal messaging protocol,

    K. Cohn-Gordon, C. Cremers, B. Dowling, L. Garratt, and D. Stebila, “A formal security analysis of the signal messaging protocol,”Journal of Cryptology, vol. 33, pp. 1914–1983, 2020

    1914

  38. [47]

    A formal analysis of apple’s iMessage PQ3 protocol,

    F. Linker, R. Sasse, and D. Basin, “A formal analysis of apple’s iMessage PQ3 protocol,” Cryptology ePrint Archive, Paper 2024/1395,

    2024

  39. [48]

    Security analysis of the imessage pq3 protocol,

    D. Stebila, “Security analysis of the imessage pq3 protocol,”Cryptology ePrint Archive, 2024

    2024

  40. [49]

    Symbolically analyzing security protocols using tamarin,

    D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Symbolically analyzing security protocols using tamarin,”ACM SIGLOG News, vol. 4, no. 4, pp. 19–30, 2017

    2017

  41. [50]

    Quantum key distribution in the classical authenticated key exchange framework,

    M. Mosca, D. Stebila, and B. Ustao ˘glu, “Quantum key distribution in the classical authenticated key exchange framework,” inPost-Quantum Cryptography: 5th International Workshop, PQCrypto 2013, Limoges, France, June 4-7, 2013. Proceedings 5. Springer, 2013, pp. 136–154

    2013

  42. [51]

    A hierarchy of authentication specifications,

    G. Lowe, “A hierarchy of authentication specifications,” inProceedings 10th computer security foundations workshop. IEEE, 1997, pp. 31–43

    1997

  43. [52]

    Time-shift attack in practical quantum cryptosystems,

    B. Qi, C.-H. F. Fung, H.-K. Lo, and X. Ma, “Time-shift attack in practical quantum cryptosystems,”arXiv preprint quant-ph/0512080, 2005

    2005 arXiv

  44. [53]

    Quantum hacking: Experimental demonstration of time-shift attack against prac- tical quantum-key-distribution systems,

    Y . Zhao, C.-H. F. Fung, B. Qi, C. Chen, and H.-K. Lo, “Quantum hacking: Experimental demonstration of time-shift attack against prac- tical quantum-key-distribution systems,”Physical Review A—Atomic, Molecular, and Optical Physics, vol. 78, no. 4, p. 042333, 2008. [54]Quantum...

    2008

  45. [58]

    Quantitative risk analysis of network time protocol (ntp) spoofing attacks,

    A. R. Mahlous, “Quantitative risk analysis of network time protocol (ntp) spoofing attacks,”IEEE Access, 2024

    2024

  46. [59]

    A devil of a time: How vulnerable is ntp to malicious timeservers?

    Y . Perry, N. R. Schiff, and M. Schapira, “A devil of a time: How vulnerable is ntp to malicious timeservers?” inNDSS, 2021

    2021

  47. [60]

    Secure two-way fiber-optic time transfer against sub-ns asymmetric delay attack with clock model-based detec- tion and mitigation scheme,

    Y . Li, J. Hu, Y . Pan, W. Huang, L. Ma, J. Yang, S. Zhang, Y . Luo, C. Zhou, C. Zhanget al., “Secure two-way fiber-optic time transfer against sub-ns asymmetric delay attack with clock model-based detec- tion and mitigation scheme,”IEEE Transactions on Instrumentation and Mea...

    2023

  48. [62]

    Qiskit: An open-source framework for quantum computing,

    IBM Quantum, “Qiskit: An open-source framework for quantum computing,” 2025, accessed: 2025-01-07. [Online]. Available: https: //www.ibm.com/quantum/qiskit

    2025

  49. [63]

    Formal verification of the etsi proposal on a standard qkd protocol,

    T. Pr ´evost, B. Martin, and O. Alibart, “Formal verification of the etsi proposal on a standard qkd protocol,” inGTMFS 2024, 2024

    2024

  50. [64]

    Security proof of practical quantum key distribution with detection-efficiency mismatch,

    Y . Zhang, P. J. Coles, A. Winick, J. Lin, and N. L ¨utkenhaus, “Security proof of practical quantum key distribution with detection-efficiency mismatch,”Physical Review Research, vol. 3, no. 1, p. 013076, 2021

    2021

  51. [65]

    Simple analysis of security of the bb84 quantum key distribution protocol,

    H.-Y . Su, “Simple analysis of security of the bb84 quantum key distribution protocol,”Quantum Information Processing, vol. 19, no. 6, p. 169, 2020

    2020

  52. [66]

    Security proof for variable-length quantum key distribution,

    D. Tupkary, E. Y .-Z. Tan, and N. L ¨utkenhaus, “Security proof for variable-length quantum key distribution,”Physical Review Research, vol. 6, no. 2, p. 023002, 2024

    2024

  53. [67]

    Muckle+: End-to-end hybrid authenticated key exchanges,

    S. Bruckner, S. Ramacher, and C. Striecks, “Muckle+: End-to-end hybrid authenticated key exchanges,” Cryptology ePrint Archive, Paper 2023/653, 2023. [Online]. Available: https://eprint.iacr.org/2023/653

    2023

  54. [68]

    Quantum authenticated key expansion with key recycling,

    W. Y . Kon, J. Chu, K. H. Y . Loh, O. Alia, O. Amer, M. Pistoia, K. Chakraborty, and C. Lim, “Quantum authenticated key expansion with key recycling,”arXiv preprint arXiv:2409.16540, 2024

    2024 arXiv

  55. [69]

    Security and application of semi-quantum key distribution protocol for users with different quantum capabilities,

    C.-Q. Ye, J. Li, X.-B. Chen, Y . Hou, and Z. Wang, “Security and application of semi-quantum key distribution protocol for users with different quantum capabilities,”EPJ Quantum Technology, vol. 10, no. 1, pp. 1–23, 2023

    2023

  56. [70]

    Security of quantum key distribution with imperfect phase randomisa- tion,

    G. Curr ´as-Lorenzo, S. Nahar, N. L ¨utkenhaus, K. Tamaki, and M. Curty, “Security of quantum key distribution with imperfect phase randomisa- tion,”Quantum Science and Technology, vol. 9, no. 1, p. 015025, 2023

    2023

  57. [71]

    Side-channel security of practical quantum key distribution,

    C. Jiang, X.-L. Hu, Z.-W. Yu, and X.-B. Wang, “Side-channel security of practical quantum key distribution,”Physical Review Research, vol. 6, no. 1, p. 013266, 2024. [72]Quantum Key Distribution (QKD); Use Cases, ETSI Std. ETSI GS QKD 002 V1.1.1, Jun. 2010. [Online]. Available...

    2024

  58. [72]

    Available: https://www.itu.int/dms pub/itu-t/opb/fg/ T-FG-QIT4N-2021-D2.5-PDF-E.pdf

    [Online]. Available: https://www.itu.int/dms pub/itu-t/opb/fg/ T-FG-QIT4N-2021-D2.5-PDF-E.pdf

    2021

  59. [85]

    Security considerations for quantum key distribution network,

    ITU-T, “Security considerations for quantum key distribution network,” ITU-T, Tech. Rep. XSTR-SEC-QKD, Mar. 2020, published by ITU Telecommunication Standardization Sector (ITU-T). [Online]. Available: https://www.itu.int/dms pub/itu-t/opb/ tut/T-TUT-QKD-2020-1-PDF-E.pdf

    2020

  60. [86]

    Quantum key distribution network protocols: Key management layer, QKDN control layer and QKDN management layer,

    H. Qin, P. Huang, and H. Wu, “Quantum key distribution network protocols: Key management layer, QKDN control layer and QKDN management layer,” ITU-T Focus Group on Quantum Information Technology for Networks (FG QIT4N), Tech. Rep. Technical Report FG QIT4N D2.3.2, Nov. 2021. [...

    2021

  61. [87]

    Standardization outlook and technology maturity: Quantum key distribution network,

    Z. Ma, T. Frantz, T. Laenger, A. Poppe, and D.-H. Sim, “Standardization outlook and technology maturity: Quantum key distribution network,” ITU-T Focus Group on Quantum Information Technology for Networks (FG QIT4N), Tech. Rep. Technical Report FG QIT4N D2.5, Nov

  62. [2021]

    Available: https://www.itu.int/dms pub/itu-t/opb/fg/ T-FG-QIT4N-2021-D2.3.1-PDF-E.pdf

    [Online]. Available: https://www.itu.int/dms pub/itu-t/opb/fg/ T-FG-QIT4N-2021-D2.3.1-PDF-E.pdf

    2021

  63. [2024]

    Available: https://eprint.iacr.org/2024/1395

    [Online]. Available: https://eprint.iacr.org/2024/1395

    2024

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.