Paper study set: 8 recommendations, 11 specifications and 4 technical reports.
The security question
4
Are QKD specifications ready for secure deployment?
Suppose the hardware constraints were solved today.
Would the published procedures be sufficient to build a secure system tomorrow?
Not quite yetThe modeled procedures admit secrecy or authentication failures.
Standards-grounded symbolic models under Eve⁺, ideal primitives and single-session scope.
Prepare-and-measure QKD
5
Prepare. Send. Measure.
AlicePrepare
BobMeasure
QUANTUM CHANNEL
│
╱
─
╲
Bits + preparation bases0 1 1 0 + × + ×
Measurement bases+ + + ×
Bits + preparation bases0 1 1 0 + × + ×
Measurement bases+ + + ×
Alice+×+××++×
Bob+++×++××
Disclose bases. Keep bit values private.
Alice+×+××++×
Bob+++×++××
Keep0×10×0×1
Matching bases → sifted bits.
Random bits + random bases
Qubits travel to Bob’s measurement station
Classical channel: authenticated basis exchange
Discard incompatible positions
BB84-style protocol shape with schematic bits and bases. Later attacks change the event order.
Entanglement-based QKD
6
One pair. Two measurement records.
AliceMeasure
BobMeasure
Pair sourceUntrusted external source
•
•
Chosen basis+ × +
Chosen basis× + +
a₁a₂a₃a₄
b₁b₂b₃b₄
CHSH
Correlations from the intended pairs
Distribute the two members of each pair
Each party measures its qubit
Compare sampled correlations
This model uses an untrusted external source. The records are illustrative, not a computed CHSH statistic.
The QKD procedure
7
From observations to a shared key
01
Sifting
02
Parameter estimation
03
Reconciliation
04
Privacy amplification
Raw observations
Alice01101001
Bob00101101
Compatible bases
Alice010001
Bob010101
Keep compatible positions
Sifted observations
Alice010001
Bob010101
Data for reconciliation
Alice1000
Bob1010
↓ 01Sample → disturbance check
Abort if disturbance is too high
Remaining observations
Alice1000
Bob1010
Reconciled data
Alice1000
Bob1000
Correct discrepancies through classical messages
Reconciled data
Alice1000
Bob1000
Final key
Alicek₁k₂
Bobk₁k₂
Apply privacy amplification
Schematic bit rows. Values and lengths are illustrative.
Modeled choices: Alice-first or Bob-first bases, with forward, reverse or two-way reconciliation.
Formal verification
8
Specifications, state machines and traces
Formal verification checks the executions allowed by a precise model.
Ask whether an allowed trace violates a security requirement.
Schematic illustration. The guarantee is limited to the model and its assumptions.
From classical protocols to QKD
9
Find the path that breaks the guarantee
Executions allowed by the model
Start
Property fails
Concrete trace
1
Initial state
2
Permitted actions
3
Violated guarantee
Specify the procedure, attacker choices and security question.
A counterexample is one allowed execution that fails the property.
Inspect the sequence to understand how the failure happens.
Schematic illustration. Verification is within the specified model and assumptions.
Classical precedent: TLS 1.3
10
A valid signature in the wrong session
AliceClient
CharlieAttacker acting as server
BobTarget server
SESSION 1: PSK 1
SESSION 2: PSK 2
✓Alice’s valid signature
The resumption transcripts match, but the session keys differ
Missing binding to the intended server / session
Alice intends to authenticate in her session with Charlie.
Charlie obtains the signature, then re-encrypts it for Bob.
Bob accepts it: Charlie impersonates Alice.
Proposed delayed-authentication extension to draft 10 with PSK resumption. Base draft-10 verification was positive. The authors report a context-binding change in draft 11.
Classical precedent: EMV
11
From a model trace to a terminal test
01: Formal discovery
Tamarin model
PIN bypass path
02: Experimental validation
Altered data
No PIN
Studied Visa card
Real payment terminal
The model exposed a path that bypassed cardholder verification.
Separate experiment: altered data claims “device verified.”
2020/2021 study of selected Visa contactless products. Physical or proximity access to the card required.
Modeling challenges
12
What makes QKD modeling difficult?
Informal procedure textMake ordering choices and assumptions explicit.
Stateful sessionsPreserve how measurements affect later messages.
Probabilistic operationsAbstract selected dependencies for symbolic analysis.
This abstraction excludes amplitudes, channel noise and coherent quantum strategies.
From classical protocols to QKD
13
Measurement shapes the next decision
QUANTUM OBSERVATION
SYMBOLIC CLASSICAL CHECK
Measurement
Measured data
Consistent?
Announced data
Continue
Abort
A measurement produces data
The check uses measured and announced data
Consistency controls the next step
Symbolic dependency in the paper’s model. Physical behavior is abstracted.
Threat and scope
14
The Eve⁺ threat model
Classical network
Delay, suppress, replay
Control the network while valid MACs remain unforgeable.
Quantum channel
Store, measure, inject
Prepare fresh qubits from known classical data.
An unknown qubit cannot be copied.
Ideal primitives. Eve⁺ cannot forge a valid authenticated message.
Threat and scope
15
The model boundary
One bounded QKD session per modeled instance.
The analysis permits unbounded protocol instances. This does not establish security across successive sessions.
Single session. Coherent strategies, device faults and cross-session key management excluded.
Why Tamarin fits the model
16
Classical operations and security questions
Symbolic operations
Hashing, encryption, signatures
Idealized classical cryptographic operations.
Execution logic
Ask what can happen
Can an attacker learn a key? Did the intended peer participate?
Tamarin capabilities, not a list of QVerify built-ins.
Why Tamarin fits the model
17
Custom quantum operations
PM preparation
Associate raw data with its preparation basis.
Measurement
Known matching basis makes raw data derivable.With a fresh basis, the symbolic operation does not derive the raw value.
Consistency checks
Use measurement-derived data to continue or abort.EB uses pair distribution and tracked pair state.
Selected dependencies only. No amplitudes, noise distributions or coherent behavior.
Why Tamarin fits the model
18
Stored state and allowed next steps
One stored qubit is an available resource.
Measure it or forward it. Either step consumes that same modeled resource.
Ask whether disclosure can precede measurement. Completion must remain possible in at least one run.
Consumable symbolic state. Ordering restrictions are assumptions.
Before the findings
19
The security requirements
A completion sanity checkCan both parties finish at least one modeled run?
Key secrecyCan the attacker learn the generated key without detection?
Peer authenticationDoes completion correspond to the intended peer, with agreement on the session and key?
Secrecy and authentication are separate goals. Executability checks that the model can run.
Security requirements
20
Increasing authentication guarantees
When Alice completes, apparently with Bob…
01Bob participatedBob ran this protocol.
02Bob intended AliceBob ran it apparently with Alice.
03Roles and data agreeThe paper checks matching session and key.
Each level adds a requirement to the previous one.
Lowe’s hierarchy, as used by the paper. The strongest check shown does not require unique matching runs.
V1: Subverted Entanglement Injection
21
V1: missing synchronization check
Bob can disclose his bases before Alice starts the session.
The modeled procedure does not verify consistent qubit receipt times.
EB procedure under Eve⁺. Symbolic, single-session model with ideal primitives.
V1: Subverted Entanglement Injection
22
Bob advances while Alice waits
AliceDelayed
Eve⁺Source under attacker control
BobSession advances
QUANTUMAUTHENTICATED CLASSICAL
q_A
q_B
clock offset
k_B rawBob has measured
Qubit batches shown schematically
Eve⁺ controls the source and introduces a clock offset
Retain q_A, then send q_B to Bob
Bob measures while Alice remains delayed
EB under Eve⁺. Symbolic, single-session model with ideal primitives.
V1: Subverted Entanglement Injection
23
Bob’s basis enables Eve’s measurement
AliceStill delayed
Eve⁺Retained qubit
BobHas measured
QUANTUMAUTHENTICATED CLASSICAL
q_A
b_B
k_B′ rawCorrelated with Bob
k_B rawraw data
Qubit batches shown schematically
Eve⁺ still holds q_A without measuring it
Bob announces b_B. Eve⁺ reads the valid public message
Measure the retained qubit in Bob’s disclosed basis
Correlated raw data under Eve⁺ in the symbolic, single-session model.
V1: Subverted Entanglement Injection
24
Replacement qubits carry known data
AliceReceives fresh qubits
Eve⁺Knows preparation data
BobContinues processing
QUANTUMAUTHENTICATED CLASSICAL
k_B′ rawraw data
fresh q_A′
public processing
k_ABEve⁺ derives the key
k_ABAlice
k_ABBob
Qubit batches shown schematically
Known raw data and b_B determine a fresh encoding
Prepare q_A′ and send it to Alice
Public post-processing lets Eve⁺ derive the session key
All three modeled EB secrecy rows fail. Same Eve⁺, symbolic, single-session scope.
V1: Subverted Entanglement Injection
25
V1 simulation evidence
Symbolic trace compatible with simulated results
The paper reports indistinguishable CHSH error distributions for the attack and noisy honest baseline.
CHSH checks can pass.
Four Aer trials. Noiseless attack circuits. Setup-specific evidence, not deployment validation.
V2: Basis-Deferred Measurement
26
Disclosure before measurement
AlicePrepared q_A
Eve⁺Store, then measure
BobReceives after Eve measures
QUANTUMAUTHENTICATED CLASSICAL
stored q_A
b_A
k_A rawEve⁺ learns raw data
fresh q_A′
Qubit batches shown schematically
Intercept q_A and keep it unmeasured
Alice discloses b_A before Bob measures
Eve⁺ measures q_A in the now-known basis
Prepare fresh q_A′ from known data, then forward it to Bob
Selected A2B configuration under Eve⁺. Fresh preparation, never cloning.
V2: Basis-Deferred Measurement
27
V2: the generated key becomes known
Public post-processing lets Eve⁺ derive the session key.
CM1 requires measurement and authenticated commitment before basis disclosure.
All three A2B secrecy rows fail under Eve⁺ in the symbolic, single-session model.
V3: Message Reflection
28
V3: authenticated data lacks peer context
What verifies
The sampled data and its MAC
The attacker returns the valid message unchanged.
What is missing
Expected peer and message direction
Sender, receiver, role and session context.
MAC remains valid. The modeled input omits context binding.
V3: Message Reflection
29
Bob receives his own sample
AliceNot participating
Eve⁺Reflects the message
BobChecks the valid MAC
QUANTUMAUTHENTICATED CLASSICAL
q_Eve
sample + MAC
same sampleSelf-comparison
Qubit batches shown schematically
Eve⁺ drives Bob with attacker-generated qubits
Bob sends his sampled data with a valid MAC
Reflect the identical message. Bob compares his sample with itself
MAC unchanged. Agreement fails under Eve⁺ in the modeled session.
V3: Message Reflection
30
Completion without the intended peer
Bob completes from inputs that do not establish Alice’s participation.
CM2 binds identities, roles and session context along with the authenticated data.
Both PM TWEC rows fail agreement under Eve⁺ in the symbolic, single-session model. No separate V3 secrecy attribution.
Countermeasures: CM1 and CM2
31
Explicit procedure requirements
Close the timing window. Bind the authenticated context.
CM1: Both parties measure, then send MAC-protected commitments, then disclose bases.
CM2: Authenticate sender, receiver, roles, session context and data together.
CM1 commitment payload and physical attestation mechanism unspecified.
Countermeasures: CM1 and CM2
32
Re-verification of the repaired models
9
repaired target models
Secrecy and agreement checks verify.
CM1 + CM2. Quantum subroutines unchanged.
Paper-reported result under Eve⁺ and the same symbolic, single-session scope.
The reusable contribution
33
A reusable family of QKD models
3 EB configurations
Reconciliation choices
Forward, reverse or two-way.
6 PM configurations
Basis order × reconciliation
Alice first or Bob first, with the three reconciliation choices.
Reusable roles, attacker fragments, restrictions and security checks.
Nine studied configurations under Eve⁺, not every flag combination.
The reusable contribution
34
A reusable analysis workflow
01
GenerateMake procedure choices explicit.
02
VerifyAsk the security question.
03
InspectRead the concrete attack trace.
04
RepairChange the procedure and check again.
QVerify provides models, templates, scripts and reports.
Demonstrated for the studied QKD family. Extension beyond it was not evaluated.
Scope and specification requirements
35
What the evidence establishes
Evidence
Specification-level findings and repairs
Formal attack traces. V1 Aer evidence under its setup. Repaired symbolic checks.
Outside the analysis
Physical and deployment guarantees
Coherent strategies and device faults. Cross-session key management. Adequacy of added deployment mechanisms.
Khwarizmi
q_A
