arxiv: 2605.11767 · v1 · submitted 2026-05-12 · 🪐 quant-ph

Recognition: 2 theorem links

· Lean Theorem

Security of decoy-state quantum key distribution with correlated bit-and-basis encoders

Guillermo Curr\'as-Lorenzo , Margarida Pereira , Alessandro Marcomini , Kiyoshi Tamaki , Marcos Curty

Authors on Pith no claims yet

Pith reviewed 2026-05-13 05:55 UTC · model grok-4.3

classification 🪐 quant-ph

keywords quantum key distributiondecoy-state BB84finite-key securitycoherent attackscorrelated encodersbit-and-basis encodersecurity proofspractical QKD

0 comments

The pith

A finite-key security proof for decoy-state BB84 QKD incorporates correlations from Alice's bit-and-basis encoder using only partial characterization of those correlations.

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

This paper establishes a security proof for practical quantum key distribution systems that use decoy states in the BB84 protocol. The proof works against general coherent attacks and finite key lengths, but it allows for the fact that the modulator introduces correlations between successive rounds. Importantly, the proof requires only a partial model of those correlations rather than full knowledge of the encoder's behavior. A sympathetic reader would care because real devices always have such memory effects, and previous proofs assumed independence that does not hold in practice. If true, this closes a gap between theory and implementable QKD.

Core claim

The authors prove that a finite-key security bound for decoy-state BB84 can be established against general coherent attacks even when Alice's bit-and-basis encoder introduces correlations between successive pulses, provided those correlations are partially characterized.

What carries the argument

The partial characterization of the correlated encoder, which allows bounding the effect on the emitted states without full knowledge of the memory effects.

If this is right

Practical QKD modulators with memory effects can now receive security proofs without assuming round-by-round independence.
The analysis applies directly to finite block sizes, making it usable for real key generation rates.
Only partial knowledge of the correlations reduces the experimental effort required to certify a device.
The bounds remain valid against the strongest class of attacks, general coherent attacks by an eavesdropper.

Where Pith is reading between the lines

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

Similar partial-modeling approaches could extend to other QKD protocols that suffer from device memory effects.
This suggests a path toward security proofs that treat the full history of the encoder rather than assuming Markovian behavior.
One could validate the partial characterization by comparing the proof bounds against full numerical simulations of the encoder dynamics.

Load-bearing premise

The correlations from the bit-and-basis encoder admit a partial characterization that is sufficient for the security bounds to hold against general coherent attacks.

What would settle it

An experimental demonstration of a specific correlation pattern in the encoder that exceeds the partial model and permits an eavesdropper to extract more key information than the derived bound allows.

read the original abstract

Practical quantum key distribution (QKD) modulators inevitably introduce correlations, causing the state emitted in a given round to depend on the setting choices made in previous rounds. These correlations break the round-by-round independence structure on which many widely used security proof techniques rely, leaving a significant gap between available theoretical guarantees and the reality of practical implementations. In this work, we develop a finite-key security proof for decoy-state BB84 against general coherent attacks that rigorously incorporates correlations introduced by Alice's bit-and-basis encoder, while requiring only partial characterization of such correlations.

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.

Desk Editor's Note private letter to a colleague

This paper gives a finite-key proof for decoy-state BB84 that folds a partial Markov model of encoder correlations into a modified entropy accumulation theorem, keeping the bounds valid against general coherent attacks.

read the letter

The main thing to know is that the authors close a practical gap by proving finite-key security for decoy-state BB84 without assuming round-by-round independence. They model the bit-and-basis encoder correlations as a finite-memory Markov process with bounded transition probabilities, then incorporate that structure into the phase-error estimation and decoy-state analysis via a modified entropy accumulation theorem. The resulting bounds hold against general coherent attacks as long as the observed correlation parameters stay inside the stated limits. This is a clear technical step beyond standard proofs that simply ignore or assume away modulator memory effects. They earn credit for needing only partial characterization rather than full device knowledge or perfect independence, which makes the result more relevant to real hardware. The argument avoids obvious circularity because the correlation bounds are treated as measurable inputs that can be checked separately from the key rate calculation. A minor soft spot is that the finite-memory length and transition bounds must actually be verified on the specific modulator; if real correlations are longer-range or stronger than modeled, the proof does not apply directly and the key rates would need re-derivation. The bounds are also expected to be somewhat looser than the ideal independent case, which is realistic but means experimental groups will have to invest effort in characterizing their devices. This work is for QKD security researchers and experimental teams that want tighter, more applicable finite-key guarantees. It deserves a serious referee because it supplies a concrete, checkable way to handle a documented imperfection with verifiable conditions rather than hand-waving. I would bring it to the next reading group to walk through the modified EAT step in detail.

Referee Report

0 major / 2 minor

Summary. The manuscript develops a finite-key security proof for decoy-state BB84 quantum key distribution against general coherent attacks. It incorporates correlations introduced by Alice's bit-and-basis encoder by modeling them as a finite-memory Markov process with bounded transition probabilities and integrates this partial characterization into the phase-error estimation and decoy-state analysis via a modified entropy accumulation theorem.

Significance. If the central derivation holds, the result meaningfully narrows the gap between theoretical QKD security proofs (which often assume round-by-round independence) and practical implementations that exhibit modulator correlations. The approach of requiring only partial characterization, rather than full device tomography, makes the bounds more experimentally accessible while remaining valid against coherent attacks; the explicit use of a modified entropy accumulation theorem is a technical strength that could be reused in related settings.

minor comments (2)

The abstract would benefit from a single sentence stating the concrete correlation model (finite-memory Markov with bounded transitions) so that readers immediately grasp the scope of the partial characterization.
Notation for the transition-probability bounds and the resulting phase-error correction term should be unified across the main text and appendices to avoid minor confusion when tracing the finite-key rate expression.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful reading and positive assessment of our manuscript. The referee's summary correctly identifies the core contribution: a finite-key security proof for decoy-state BB84 against coherent attacks that incorporates partial characterization of bit-and-basis encoder correlations via a finite-memory Markov model and a modified entropy accumulation theorem. We are pleased that the practical relevance and technical approach are recognized.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper presents a finite-key security proof for decoy-state BB84 that incorporates a partial characterization of bit-and-basis encoder correlations (modeled explicitly as a finite-memory Markov process with bounded transitions) into phase-error estimation and decoy-state analysis through a modified entropy accumulation theorem. This structure derives bounds directly from the stated correlation assumptions and observed statistics without reducing any central prediction or uniqueness claim to a fitted parameter or self-citation by construction. The abstract and described approach remain self-contained against external benchmarks, with no load-bearing step that equates an output to its own inputs via the paper's equations.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Review performed on abstract only; no explicit free parameters, invented entities, or ad-hoc axioms are stated. The proof presumably rests on standard BB84 and decoy-state assumptions plus finite-key analysis techniques, but these cannot be audited in detail.

axioms (2)

domain assumption Decoy-state BB84 protocol assumptions
The work extends the standard decoy-state BB84 setting.
standard math Finite-key security analysis framework
Uses established finite-key techniques for QKD.

pith-pipeline@v0.9.0 · 5396 in / 1348 out tokens · 40661 ms · 2026-05-13T05:55:25.321177+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

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

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

we develop a finite-key security proof for decoy-state BB84 against general coherent attacks that rigorously incorporates correlations introduced by Alice's bit-and-basis encoder, while requiring only partial characterization of such correlations
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Lemma 2 ... partition the N rounds into lc+1 groups of mutually independent variables and apply a Chernoff-type bound within each group

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.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Numerical security analysis for practical quantum key distribution
quant-ph 2026-05 unverdicted novelty 6.0

A numerical framework proves finite-key security for practical decoy-state QKD systems with transmitter and receiver imperfections including non-IID signals.

Reference graph

Works this paper leans on

53 extracted references · 53 canonical work pages · cited by 1 Pith paper

[1]

From the perspective of all other systems, any measurement on Alice’s local register is equivalent to a partial trace, which is basis-independent

The measurement of coin registersC k in the Hadamard basis{|+⟩,|−⟩}for the trash-sifted rounds (step 5a) does not affect any announced information, since the outcome of this measurement is never revealed. From the perspective of all other systems, any measurement on Alice’s local register is equivalent to a partial trace, which is basis-independent. This ...

work page
[2]

The measurement of the photon-number registersM k (step 6) is similarly a local operation on Alice’s side whose outcome is not announced, and can therefore be placed at any point in the protocol without affecting observable statistics; it is included at this stage for notational convenience

work page
[3]

sifted” or “unsifted

In the actual protocol, Alice’s keep/trash decision is made only for detected roundsk∈ D. In the source-replaced protocol, however, Alice makes this decision forallroundsk∈ {1, . . . , N}, but only announces it for detected rounds. Since the keep/trash assignment for undetected rounds is never revealed, this modification does not affect any announced info...

work page
[4]

Alice prepares her global source replacement state|Ψ N ⟩CN 1 AN 1 I N 1 M N 1 T N 1

work page
[5]

trash” with probability (1−p keep), and to “sifted

For each roundk∈ {1, ..., N}, Alice measures the photon number systemM k to learn the photon number mk. Ifm k = 1, Alice assigns the round to “trash” with probability (1−p keep), and to “sifted” with probability 1/2. Then, if the round is assigned to both “trash” and “sifted”, Alice measures the coin systemC k in the{|+⟩,|−⟩}basis. We denote byn trash,sif...

work page
[6]

We define a fictitious source with correlations truncated at a finite lengthl eff c

work page
[7]

We prove security for the fictitious source using the tools already established

work page
[8]

11 Lifting security from bounded to unbounded correlations The following lemma, which is model-independent, provides the mechanism for step 3

We bound the trace distance between the actual and fictitious source-replacement states, and lift the security guarantee to the actual source via Lemma 4 below. 11 Lifting security from bounded to unbounded correlations The following lemma, which is model-independent, provides the mechanism for step 3. Lemma 4(Unbounded correlations [21]).Let|Ψ (∞) N ⟩CN ...

work page
[9]

Note that we can divideZ nK A =Z nK,(1) A Z nK,(rest) A ,X nK A =X nK,(1) A X nK,(rest) A andX nK B =X nK,(1) B X nK,(rest) B based on the photon number

Proof of Theorem 1 Proof.LetWbe the classical register containing the outcome of the announced data vector⃗ n, let⃗ mbe a random vector containing the outcomes of Alice’s measurements on the photon number registersM N 1 (which are not announced), let Ω(⃗ n, ⃗ m) be the event in which⃗ n=⃗ n,⃗ m=⃗ mis observed, letρ|Ω(⃗ n, ⃗ m)be the state shared by Alice,...

work page
[10]

Proof of Lemma 1 Proof.To prove this, we consider a scenario that yields identical statistics for the single-photon sifted rounds as the Phase-error estimation protocol, but in which Alice and Bob do things in a different order. Namely:

work page
[11]

Alice and Bob determine the set of detected sifted rounds withm k = 1,D (1) sifted

work page
[12]

Lete k ∈ {err, err}be the outcome of this measurement

For each roundk∈ D (1) sifted: (a) Alice and Bob perform the joint POVM{ˆmerr,I−ˆmerr}, where ˆmerr =|0 X ⟩ ⟨0X |A ⊗G(X) 1 +|1X ⟩ ⟨1X |A ⊗G(X) 0 . Lete k ∈ {err, err}be the outcome of this measurement

work page
[13]

Then, ift k = keep, Alice measures systemC k in the{|Z⟩,|X⟩} ≡ {|0⟩,|1⟩}basis, obtaining an outcomec k ={Z, X}

Alice choosest k = keep with probabilityp keep ort k = trash otherwise. Then, ift k = keep, Alice measures systemC k in the{|Z⟩,|X⟩} ≡ {|0⟩,|1⟩}basis, obtaining an outcomec k ={Z, X}. Conversely, ift k = trash, Alice measures systemC k in the{|+⟩,|−⟩}basis, obtaining an outcomec k ={+,−}

work page
[14]

15 The equivalence is due to the following

Alice and Bob perform all their other measurements. 15 The equivalence is due to the following. By the principle of deferred measurement, we may assume that all classical coins (keep/trash, sifted/unsifted) are drawn at the start, and measurements on disjoint subsystems commute. In the original phase-error protocol, on each detected keep-sifted round (k∈ ...

work page
[15]

If this does not hold, a very similar result can be derived by making trivial modifications

Proof of Lemma 2 Proof.For simplicity, we assume that the total number of roundsNis a multiple of (l c + 1). If this does not hold, a very similar result can be derived by making trivial modifications. Partition the rounds into (l c + 1) sets according toI w ={k:k≡wmodl c + 1}, and express ntrash,sifted,−,(1) = lcX w=0 n(Iw) trash,sifted,−,(1),(A23) where...

work page
[16]

Alice prepares her global quantum coin state|Ψ N ⟩CN 1 AN 1 I N 1 M N 1 T N 1

work page
[17]

For each roundk̸∈I w, Alice measures the coin systemC k in the{|Z⟩,|X⟩}basis to obtainα k, and then measures systemA k in the{|0 αk ⟩,|1 αk ⟩}basis to obtaina k

work page
[18]

trash” with probability (1−p keep), and to “sifted

For each roundk∈I w, Alice measures the photon number systemM k to learn the photon numberm. If m= 1, Alice assigns the round to “trash” with probability (1−p keep), and to “sifted” with probability 1/2. Then, if the round is assigned to both “trash” and “sifted”, Alice measures the coin systemC k in the {|+⟩,|−⟩}basis. Note that the measurements on the r...

work page
[19]

Proof of Theorem 2 Proof.We prove this by considering the complement of the failure events and applying a union bound. First, we define the “good” events: •Ω A: the event where the bound from Lemma 1 holds •Ω C: the event where the bound from Lemma 2 holds •Ω dec: the complement of Ω dec,fail, i.e., the event where the decoy-state bounds hold From the lem...

work page
[20]

Proof of Lemma 5 Proof.We bound ∆ U coin by analyzing the overlaps appearing in its definition in Eq. (17). Recall from Eq. (18) that |Ξak,αk|a¯k,α¯k ⟩Tk I k+lc k+1 M k+lc k+1 T k+lc k+1 =|ψ (1) ak k−lc , αk k−lc ⟩Tk ⊗ k+lcO j=k+1 |Ψaj j−lc , αj j−lc ⟩Ij Mj Tj ,(A47) wherea ¯k = (ak−1 k−lc , ak+lc k+1 ) andα ¯k = (αk−1 k−lc , αk+lc k+1 ). This state facto...

work page
[21]

The objective is thus to boundFfrom below

Proof of Lemma 6 Proof.Since both states are pure, the trace distance equalsT= √ 1−F 2, whereF= ⟨Ψ(lc) N |Ψ(∞) N ⟩ is the fidelity. The objective is thus to boundFfrom below. a. Inner product of the global states.Both|Ψ (∞) N ⟩and|Ψ (lc) N ⟩have the structure given in Eq. (6), with identical coin, qubit, and intensity/photon-number registersC k,A k,I k,M ...

work page
[22]

Gottesman, H.-K

D. Gottesman, H.-K. Lo, N. L¨ utkenhaus, and J. Preskill, Security of quantum key distribution with imperfect devices, Quantum Inf. Comput.4, 325 (2004)

work page 2004
[23]

C.-H. F. Fung, K. Tamaki, B. Qi, H.-K. Lo, and X. Ma, Security proof of quantum key distribution with detection efficiency mismatch, Quantum Information & Computation9, 131 (2009)

work page 2009
[24]

Tamaki, M

K. Tamaki, M. Curty, G. Kato, H.-K. Lo, and K. Azuma, Loss-tolerant quantum cryptography with imperfect sources, Phys. Rev. A90, 052314 (2014)

work page 2014
[25]

Pereira, G

M. Pereira, G. Kato, A. Mizutani, M. Curty, and K. Tamaki, Quantum key distribution with correlated sources, Sci. Adv. 6, eaaz4487 (2020)

work page 2020
[26]

Curr´ as-Lorenzo, M

G. Curr´ as-Lorenzo, M. Pereira, G. Kato, M. Curty, and K. Tamaki, Security framework for quantum key distribution with imperfect sources, Optica Quantum3, 525 (2025)

work page 2025
[27]

Tupkary, S

D. Tupkary, S. Nahar, P. Sinha, and N. L¨ utkenhaus, Phase error rate estimation in QKD with imperfect detectors, Quantum 9, 1937 (2025)

work page 1937
[28]

Sixto, ´A

X. Sixto, ´A. Navarrete, M. Pereira, G. Curr´ as-Lorenzo, K. Tamaki, and M. Curty, Quantum key distribution with imper- fectly isolated devices, Quantum Sci. Technol.10, 035034 (2025)

work page 2025
[29]

Kamin, J

L. Kamin, J. Burniston, and E. Y.-Z. Tan, R´ enyi security framework against coherent attacks applied to decoy-state QKD (2025), arXiv:2504.12248 [quant-ph]

work page arXiv 2025
[30]

Marwah and F

A. Marwah and F. Dupuis, Proving security of BB84 under source correlations (2024), arXiv:2402.12346 [quant-ph]

work page arXiv 2024
[31]

Nahar and N

S. Nahar and N. L¨ utkenhaus, Imperfect detectors for adversarial tasks with applications to quantum key distribution (2025), arXiv:2503.06328 [quant-ph]

work page arXiv 2025
[32]

Gr¨ unenfelder, A

F. Gr¨ unenfelder, A. Boaron, D. Rusca, A. Martin, and H. Zbinden, Performance and security of 5 GHz repetition rate polarization-based quantum key distribution, Appl. Phys. Lett.117, 144003 (2020)

work page 2020
[33]

Agulleiro, F

A. Agulleiro, F. Gr¨ unenfelder, M. Pereira, G. Curr´ as-Lorenzo, H. Zbinden, M. Curty, and D. Rusca, Modeling and Char- acterization of Arbitrary Order Pulse Correlations for Quantum Key Distribution (2025), arXiv:2506.18684 [quant-ph]

work page arXiv 2025
[34]

Christandl, R

M. Christandl, R. K¨ onig, and R. Renner, Postselection Technique for Quantum Channels with Applications to Quantum Cryptography, Phys. Rev. Lett.102, 020504 (2009)

work page 2009
[35]

Nahar, D

S. Nahar, D. Tupkary, Y. Zhao, N. L¨ utkenhaus, and E. Y.-Z. Tan, Postselection Technique for Optical Quantum Key Distribution with Improved de Finetti Reductions, PRX Quantum5, 040315 (2024)

work page 2024
[36]

Renner, Symmetry of large physical systems implies independence of subsystems, Nature Phys3, 645 (2007)

R. Renner, Symmetry of large physical systems implies independence of subsystems, Nature Phys3, 645 (2007)

work page 2007
[37]

Arqand and E

A. Arqand and E. Y.-Z. Tan, Marginal-constrained entropy accumulation theorem (2025), arXiv:2502.02563 [quant-ph]

work page arXiv 2025
[38]

Tomamichel and R

M. Tomamichel and R. Renner, Uncertainty Relation for Smooth Entropies, Phys. Rev. Lett.106, 110506 (2011)

work page 2011
[39]

Tomamichel, C

M. Tomamichel, C. C. W. Lim, N. Gisin, and R. Renner, Tight finite-key analysis for quantum cryptography, Nat Commun 3, 634 (2012)

work page 2012
[40]

Tomamichel and A

M. Tomamichel and A. Leverrier, A largely self-contained and complete security proof for quantum key distribution, Quantum1, 14 (2017)

work page 2017
[41]

Koashi, Simple security proof of quantum key distribution based on complementarity, New J

M. Koashi, Simple security proof of quantum key distribution based on complementarity, New J. Phys.11, 045018 (2009)

work page 2009
[42]

Curr´ as-Lorenzo, M

G. Curr´ as-Lorenzo, M. Pereira, K. Tamaki, and M. Curty, Rigorous phase-error-estimation security framework for QKD with correlated sources (2026), arXiv:2601.08417 [quant-ph]

work page arXiv 2026
[43]

Mizutani and G

A. Mizutani and G. Kato, Security of round-robin differential-phase-shift quantum-key-distribution protocol with correlated light sources, Phys. Rev. A104, 062611 (2021)

work page 2021
[44]

Pereira, G

M. Pereira, G. Curr´ as-Lorenzo,´A. Navarrete, A. Mizutani, G. Kato, M. Curty, and K. Tamaki, Modified BB84 quantum key distribution protocol robust to source imperfections, Phys. Rev. Res.5, 023065 (2023)

work page 2023
[45]

Hwang, Quantum key distribution with high loss: Toward global secure communication, Physical Review Letters 91, 057901 (2003)

W.-Y. Hwang, Quantum key distribution with high loss: Toward global secure communication, Physical Review Letters 91, 057901 (2003)

work page 2003
[46]

H.-K. Lo, X. Ma, and K. Chen, Decoy State Quantum Key Distribution, Phys. Rev. Lett.94, 230504 (2005)

work page 2005
[47]

Wang, Beating the Photon-Number-Splitting Attack in Practical Quantum Cryptography, Phys

X.-B. Wang, Beating the Photon-Number-Splitting Attack in Practical Quantum Cryptography, Phys. Rev. Lett.94, 230503 (2005)

work page 2005
[48]

Lo and J

H.-K. Lo and J. Preskill, Security of quantum key distribution using weak coherent states with nonrandom phases, Quantum Inf. Comput.7, 431 (2007)

work page 2007
[49]

Curr´ as-Lorenzo, M

G. Curr´ as-Lorenzo, M. Pereira, S. Nahar, and D. Tupkary, Security of quantum key distribution with source and detector imperfections through phase-error estimation (2025), arXiv:2507.03549 [quant-ph]

work page arXiv 2025
[50]

Z. Wang, D. Tupkary, and S. Nahar, Phase error estimation for passive detection setups with imperfections and memory effects (2025), arXiv:2508.21486 [quant-ph]

work page arXiv 2025
[51]

Mannalath, V

V. Mannalath, V. Zapatero, and M. Curty, Sharp Finite Statistics for Quantum Key Distribution, Phys. Rev. Lett.135, 020803 (2025)

work page 2025
[52]

Bernstein, On a modification of Chebyshev’s inequality and of the error formula of Laplace, Ann

S. Bernstein, On a modification of Chebyshev’s inequality and of the error formula of Laplace, Ann. Sci. Inst. Sav. Ukraine, Sect. Math1, 38 (1924)

work page 1924
[53]

Boucheron, G

S. Boucheron, G. Lugosi, and P. Massart,Concentration Inequalities: A Nonasymptotic Theory of Independence(Oxford University Press, 2013)

work page 2013