Motivation
Quantum key distribution (QKD) is the first quantum information task to reach the level of mature technology, already fit for commercialization. It aims at the creation of a secret key between authorized partners connected by a quantum channel and a classical authenticated channel. The security of the key can in principle be guaranteed without putting any restriction on the eavesdropper's power. The first two sections provide a concise up-to-date review of QKD, biased toward the practical side. The rest of the paper presents the essential theoretical tools that have been developed to assess the security of the main experimental platforms (discrete variables, continuous variables and distributed-phase-reference protocols).
This mission is the statement-level formalization of The Security of Practical Quantum Key Distribution (arXiv:0802.4155v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is I.B.5: intercept-resend information and disturbance (I.B.5: intercept-resend information and disturbance, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
28 results of the paper are not stated yet, because the library lacks an interface they need:
- Paper seed, p.1: practical BB84 without decoy states, IV.B.2, Eq.(31): Operational tagged/squashed no-decoy BB84 extraction against all compatible attacks (hard)
- II.C.3: schematic finite-key bound, Eq.(7): Printed schematic claim: Prob[||rho_KE-tau_K tensor rho_E||_1>2epsilon] is bounded up to omitted constants by exp(ell-F(rho_KE,epsilon)). (source-ambiguity)
- II.E.1: phase randomization yields Poisson photon statistics, Eqs.(11)–(13): Normalized full-Fock coherent states and trace-class phase-average equality (hard)
- III.B.2.a: one-way individual-attack bound, Eqs.(21)–(22): Uniform-over-compatible individual-attack one-way EC–PA achievability (hard)
- III.B.2.b: one-way collective-attack bound, Eqs.(21),(23),(24): Uniform ccq direct/reverse extraction with half trace-distance security (hard)
- IV.B.1: BB84 photon components and optimized privacy cost, Eq.(28): Constructed photon-tagged attack states, Holevo extrema and attaining attacks (hard)
- IV.B.3: exact-parameter decoy BB84 rate and summation, Eqs.(33)–(34): Operational separately processed class extraction including vacuum contribution (hard)
- IV.B.5: safe-source EB conservative multipair bound, Eqs.(40)–(42): Safe-SPDC multipair tagging and evaluated extraction (hard)
- IV.B.5: EB qubit rate from a basis-independent source, Eq.(43): Basis-independent uncharacterized source to secure evaluated protocol (hard)
- IV.C.2: calibrated decoy upper estimate, Eq.(50): Restricted calibrated-attack upper estimate with operational comparison (hard)
- IV.C.2: calibrated no-decoy upper estimate, Eqs.(51)–(52): Feasible inferred calibrated parameters and restricted-attack upper comparison (hard)
- V.B.3: Gaussian conditional variance and mutual information, Eqs.(60)–(61): Physical Gaussian experiment and actual mutual information (hard)
- V.B.4: Eve–Alice conditional-variance tradeoff, Eqs.(62)–(65): Purification-conditioned quadrature variances and minimizing ensemble (hard)
- V.B.4: reverse-reconciled individual-attack rate, Eq.(66): Gaussian individual-attack rate and saturating entanglement-cloner construction (hard)
- V.B.4: qualitative high-loss / large-modulation noise tolerance: Source reports positivity in a high-loss (t*eta -> 0), large-modulation (v -> infinity) regime when epsilon<1/2. (source-ambiguity)
- V.B.5: computed collective Gaussian Holevo information, Eqs.(67)–(68): Actual Gaussian output and conditioned state entropies (hard)
- V.B.5: Gaussian-modulated homodyne collective security, Eq.(69): Gaussian extremality plus operational reverse-reconciled extraction (hard)
- V.B.6: conditioned binary-channel postselection, Eqs.(70)–(71): Announcement-conditioned Gaussian instrument and averaged EC–PA extraction (hard)
- VI.B.1: coherent beam-splitting attack and output states: Vacuum beam-splitter isometry on full Fock spaces (hard)
- VI.B.1: DPS beam-splitting Holevo information and rate, Eqs.(73)–(74): Full-Fock two-pulse conditional mixtures and their Holevo spectra (hard)
- VI.B.1: COW beam-splitting Holevo information and rate, Eqs.(75)–(76): Two-mode coherent/vacuum key states and their Holevo information (hard)
- VI.B.2: restricted two-pulse COW upper estimate, Eqs.(77)–(78): Reported restricted-family expression: xi=2sqrt[V(1-V)]. If exp(-mu)<=xi, I_E=1; otherwise I_E=epsilon+(1-epsilon)h((1+F_V(mu))/2), F_V=(2V-1)exp(-mu)-xisqrt(1-exp(-2mu)). K=R*(1-I_E-leak_EC(Q)), R=nu_tilde*(mutt_B*eta+2p_d). (source-ambiguity)
- VII.A–B: numerical platform and calibration comparisons: Figures 4–6 compare optimized K/nu_S for specified Table II parameter sets. BB84 curves are unconditional bounds under IV’s assumptions; CV curves concern collective attacks; COW curves concern only VI.B.2 restricted attacks. The stated calibration improvements are numerical/qualitative. (source-ambiguity)
- Appendix A: Bell-diagonal errors and Eve’s information, Eqs.(A1)–(A4): Measured Bell purification and computed conditional Eve entropies (hard)
- Appendix A: general six-state privacy cost, Eq.(A5): Six-state operational reduction with boundary-safe computed Bell Holevo cost (hard)
- Appendix A: depolarizing six-state key fraction, Eq.(A6): Depolarizing six-state secure fraction and implicit first zero (hard)
- Appendix A: BB84 entropy maximization and 11% threshold, Eqs.(A7)–(A9): BB84 entropy maximum and operational symmetry/extraction reduction (hard)
- Appendix B: qualitative four-link repeater claims: The source reports ideal R_4 proportional to t^(1/4), four memories released before T_M, three Bell measurements, an approximately 95% fidelity requirement, and effective memory transmission p_M_prime≈p_M*t^(1/4). (source-ambiguity)
Selected references