{"id":"4816c7cd-b02d-4bb6-bdd6-3c8f9d1e02a3","arxiv_id":"2608.07626","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":2,"one_line_summary":"Symbolic Tamarin models of standards-grounded QKD protocols reveal three control-plane vulnerabilities and confirm two countermeasures.","lead":"A formal verification framework uses the Tamarin tool to model ETSI and ITU-T QKD procedures, exposing three weaknesses in how classical control messages interact with the quantum phase, plus two fixes that restore the checked security properties. The relevance is that QKD security proofs silently assume classical ordering and authentication details that the standards leave open.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"V1's undetectability claim contradicts CHSH: after Eve re-encodes in Bob's announced basis, mismatched-basis correlations vanish (S≈0, at best -2), so the Qiskit comparison cannot show indistinguishability from honest EB (S≈-2.82); the Tamarin check() omits CHSH, making V1 an abstraction artifact.","rationale":"Good-faith reading: the paper is an honest artifact with a publicly available Tamarin framework, and V2/V3 are credible classical control-plane findings. However, the central claim that 'three' vulnerabilities are established under Eve+ depends on V1, and V1's physical validation contradicts elementary CHSH. The Qiskit comparison compares a noiseless attack to a noisy honest baseline, and for the described attack the CHSH parameter is far below the honest value. The symbolic check omits CHSH entirely, so the Tamarin result cannot certify undetectability. This is exactly the reader's weakest assumption. I agree with the reader's analysis; the concern is load-bearing. Given that one of three headline results fails, the REJECT verdict is appropriate as submitted, though a revision that removes or repairs V1 and focuses on V2/V3 plus the framework would be a useful contribution.","tokens_in":19473,"tokens_out":9404,"duration_ms":96102,"concrete_test":"Run the QVerify Qiskit V1 script with a standard CHSH estimator over all four Alice/Bob setting pairs (e.g., Alice 0°/45°, Bob 22.5°/67.5°, or the BB84 Z/X pair used in the repo) using noiseless attack circuits; compute S and the fraction of runs within 10% of -2√2. If S≈0 (or at best -2), the 'undetected' claim fails. Second, add an explicit CHSH-failure condition to the Tamarin EB check() in §III-A2 and re-verify Lemma 1; if the V1 counterexample disappears, the vulnerability is an artifact of the abstraction rather than a standards-level omission.","verdict_should_be":"REJECT","load_bearing_attack":"Section IV-A/V1 is load-bearing because it is one of the three 'specification-level vulnerabilities' and is the only one backed by the Qiskit validation in §IV-D. The attack procedure fixes Eve's forwarded qubit to be an eigenstate of Bob's announced basis (measure q_A in b_B, encode q'_A from k'_raw_B and b_B). For Alice's setting equal to Bob's, correlation is perfect; for any mismatched setting, Alice's outcome is random and independent, so the CHSH correlator is 0. Thus a standard CHSH test yields S≈0 (or S=-2 if the setting sets coincide), not S within 10% of -2√2. The reported indistinguishability in Figure 7(b) is therefore inconsistent with the attack as described. The symbolic check() in §III-A2 contains no CHSH term—it only requires Bob's measured qubit to match Alice's prepared qubit and the classical consistency condition—so the Tamarin falsification of Lemma 1 for EB models may be an artifact of omitting the very test that is supposed to catch unentangled/re-encoded sources. The paper's own limitation paragraph does not remedy this: V1's 'undetected' claim is a physical claim, and the only physical support is the contradictory Qiskit comparison. V2 and V3 remain plausible because they are purely classical ordering/binding omissions and do not rely on CHSH.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":19779,"tokens_out":8066,"duration_ms":78058,"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":[{"comment":"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.","section":"§IV-A, §IV-D, Fig. 7(b)"},{"comment":"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.","section":"§III-A2, check(s_A, s_B)"},{"comment":"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.","section":"§IV-A, Root Cause"},{"comment":"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.","section":"§V-B"}],"minor_comments":[{"comment":"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.","section":"Fig. 7"},{"comment":"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.","section":"Table I"},{"comment":"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.","section":"§III-A2"},{"comment":"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.","section":"§IV-D"},{"comment":"The abstract contains the typo \"ahybridprotocol\" in the first paragraph; please correct it.","section":"Abstract"}],"recommendation":"major_revision","confidential_remarks":"The paper's artifact is a genuine strength, and the V2/V3 analysis is plausible and well-supported by the symbolic model. The V1 issue is severe: the Qiskit comparison appears internally inconsistent, and the symbolic abstraction omits the Bell test that the protocol is supposed to perform. This must be resolved before the paper can be published. Given the authors' engagement with standards bodies, the V1 claim should not be circulated as established without correction."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe short version: the QVerify Tamarin pipeline is a genuine, reproducible artifact, and the V2 and V3 findings look like real specification-level issues. But V1, the subverted entanglement injection, does not survive contact with CHSH. I side with the stress-test note: the attack as described destroys mismatched-basis correlations, so the Qiskit comparison showing indistinguishability from honest EB at S≈-2.82 cannot be right, and the Tamarin model omits the Bell test from its check() predicate, so the EB secrecy failure is likely an artifact of the abstraction.\n\nWhat is actually new: the m4-templated model family spanning PM and EB QKD with authenticated classical channels, nine configurations, and four lemmas per configuration is a solid engineering contribution. The artifact is complete and documented. The basis-announcement ordering analysis (A2B vs B2A) is well done; V2 is a textbook deferred-measurement attack, and V3 (MAC reflection) is a clean role-binding omission. The proposed countermeasures, measurement commitment and identity-bound MACs, are sensible, and the Tamarin verification that they restore the lemmas is credible.\n\nWhere it softens: V1's undetectability claim is load-bearing because it is one of three headline vulnerabilities and the only one backed by the Qiskit experiment. The attack procedure has Eve encode q'_A from Bob's announced basis b_B; for any Alice setting different from b_B, Alice's outcome is random and uncorrelated with Bob's, so the CHSH correlator vanishes. You get S≈0, not within 10% of -2√2. The paper's own limitation paragraph in §VI-A does not reconcile this; it only acknowledges symbolic scope, but undetectability is a physical claim. The symbolic check() also contains no CHSH term, so the EB secrecy falsification may be an artifact of omitting the one test designed to catch that attack.\n\nNet: the framework deserves referee time, but V1 needs either a corrected simulation or an explicit acknowledgment that the attack is detectable by a standard Bell test and therefore not a spec-level vulnerability as claimed. A revised paper focusing on the pipeline and V2/V3 would be a useful contribution.","headline":"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.","tokens_in":20318,"tokens_out":3500,"would_cite":false,"duration_ms":32830,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["81P94","68Q60","94A60"],"pacs":["03.67.Dd"],"model":"deepseek-v4-flash","headline":"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…","keywords":["quantum key distribution","symbolic verification","Tamarin prover","classical control plane","entanglement-based QKD","prepare-and-measure QKD","message authentication codes","ETSI and ITU-T standards"],"falsifier":"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.","tokens_in":19215,"feed_emoji":"🔐","tokens_out":6721,"duration_ms":54488,"temperature":0.7,"pith_summary":"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.","feed_headline":"Quantum key distribution has three protocol-level security holes","feed_subtitle":"A symbolic model of ETSI and ITU-T procedures traces them to timing and message-order gaps in classical control.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"The ETSI GS QKD 005 security-proofs specification that defines the probabilistic security statement and serves as the standards grounding for the EB and PM models.","marker":"[10]"},{"why":"The ITU-T FG QIT4N quantum-layer technical report whose basis-announcement ordering is left unspecified, creating the V2 basis-deferred measurement hazard.","marker":"[36]"},{"why":"Establishes the symbolic-abstraction approach for quantum protocol verification that the paper's quantum symbolic model builds on.","marker":"[23]"},{"why":"Introduces the Tamarin Prover, the automated verification engine used to check the secrecy and agreement lemmas.","marker":"[24]"},{"why":"Defines the Dolev-Yao network attacker model that, combined with a quantum eavesdropper, forms the Eve+ threat profile.","marker":"[40]"},{"why":"Supplies Lowe's authentication hierarchy, the basis for the non-injective agreement lemmas that V3 falsifies.","marker":"[51]"},{"why":"Documents the time-shift attack that motivates the V1 timing-synchronization vulnerability in entanglement-based QKD.","marker":"[52]"},{"why":"Provides the Qiskit Aer simulator used to argue that the V1 attack's CHSH statistics are compatible with honest error distributions.","marker":"[62]"}],"fun_headline_variants":["QKD classical control gaps enable three key-recovery attacks","ETSI/ITU-T QKD specs have three classical control flaws","Quantum key distribution's weak link: classical control","Three QKD protocol holes from untracked classical messages","Quantum key distribution security hinges on classical messages"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["QKD classical control gaps enable three key-recovery attacks","ETSI/ITU-T QKD specs have three classical control flaws","Quantum key distribution's weak link: classical control","Three QKD protocol holes from untracked classical messages","Quantum key distribution security hinges on classical messages"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000635,"raw_usage":{"total_tokens":2988,"prompt_tokens":1066,"completion_tokens":1922,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":682,"completion_tokens_details":{"reasoning_tokens":1843}},"tokens_in":682,"tokens_out":1922,"duration_ms":12570,"temperature":1.0,"reasoning_tokens":1843,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T00:29:54.717162+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Quantum key distribution network protocols: Quantum layer,","cited_arxiv_id":null,"evidence_quote":"The ITU-T FG QIT4N quantum-layer technical report whose basis-announcement ordering is left unspecified, creating the V2 basis-deferred measurement hazard."},{"cited_title":"Symbolic abstractions for quantum protocol verification,","cited_arxiv_id":null,"evidence_quote":"Establishes the symbolic-abstraction approach for quantum protocol verification that the paper's quantum symbolic model builds on."},{"cited_title":"A hierarchy of authentication specifications,","cited_arxiv_id":null,"evidence_quote":"Supplies Lowe's authentication hierarchy, the basis for the non-injective agreement lemmas that V3 falsifies."},{"cited_title":"Qiskit: An open-source framework for quantum computing,","cited_arxiv_id":null,"evidence_quote":"Provides the Qiskit Aer simulator used to argue that the V1 attack's CHSH statistics are compatible with honest error distributions."}],"review_version":1}