FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq

I. INTRODUCTION

• QKD proofs combine mathematically sophisticated ingredients, while earlier QKD formalizations and classical frameworks do not provide the complete composable finite-key proof.Classical tools lack the information-theoretic and quantum foundations required for smooth-entropy bounds against unbounded quantum adversaries.Source: §I · pp. 1–2
• FVQKD delivers an end-to-end kernel-checked composable finite-key BB84 proof and reconstructs reusable proof infrastructure, including implicit side conditions in the published argument.The mechanization relies on the Rocq kernel and three standard axioms inherited from MATHCOMP-ANALYSIS.Source: §I · p. 2

II. QUANTUM KEY DISTRIBUTION

• QKD lets two parties establish a shared key whose secrecy rests on quantum mechanics rather than computational hardness.The section introduces quantum foundations, common protocol structure, and BB84 as preparation for the security analysis and protocol model.Source: §II · p. 3

A. Quantum Foundations

• Conjugate Z- and X-basis measurements make interception detectable, while fidelity and purified distance formalize closeness between quantum states for security analysis.Smooth entropies optimize over states within a purified-distance ε-ball.Source: A. Quantum Foundations · p. 3

B. Components and Variants

• QKD protocols share preparation, transmission, measurement, sifting, parameter estimation, error correction, and privacy amplification, despite differing in signals and measurement.Variants include entanglement-based protocols, six-state QKD, decoy-state methods, and detector-independent approaches.Source: B. Components and Variants · pp. 3–4

C. BB84

• BB84 prepares and measures signals, sifts matching bases, estimates errors on test bits, corrects the raw key, and hashes it to produce the final key.The prepare-and-measure and entanglement-based variants differ in preparation; their subsequent post-processing is identical.Source: C. BB84 · p. 4

A. Proof Routes

• FVQKD follows Tomamichel et al.’s smooth-entropy route, combining an entropic uncertainty relation, Serfling sampling bound, and Quantum Leftover Hash Lemma.The route targets tight composable finite-key bounds without asymptotic or de Finetti penalties.Source: A. Proof Routes · p. 4

B. Security Model

• The model gives Eve unrestricted quantum-channel control and coherent attacks across rounds, while Alice and Bob follow the protocol and keep internal computations private.Eve reads authenticated classical messages but cannot forge or modify them.Source: B. Security Model · p. 4
• The security claim depends on explicit device and channel assumptions, including side-channel freedom, source characterization, delayed measurement, basis-independent detection, and a calibrated projective X/Z endpoint.The source and measurement characterization and preparation-quality parameter must faithfully describe the devices; authentication is assumed for the classical channel.Source: B. Security Model · p. 5
• Composable security requires correctness and secrecy, with total security parameter ε bounded by εc + εs.The trace-distance secrecy criterion is universally composable.Source: B. Security Model · pp. 5–6

Proof setup

• The proof models the sifted rounds as a joint state, partitions them randomly into test and key blocks, and uses conditional min- and max-entropy to quantify secrecy and reconstruction.For classical A, 2^-Hmin(A | E) is Eve’s optimal guessing probability.Source: C. Finite-Key Bound · p. 6

Smooth entropies

• A domain condition on smoothing parameters is surfaced as a mechanization finding.The condition requires 0 ≤ ε < √Tr ρ.Source: C. Finite-Key Bound · p. 6

Entropic uncertainty

• The entropic uncertainty relation links uncertainty in the raw key to uncertainty in a conjugate string, giving a lower bound on Hε min(X | E) for privacy amplification.The preparation quality scales the uncertainty lower bound, while parameter estimation bounds the conjugate-string entropy through observed errors.Source: C. Finite-Key Bound · p. 6

Privacy amplification

• The Quantum Leftover Hash Lemma converts sufficient smooth min-entropy into a nearly uniform key against quantum side information using a two-universal hash family.The final bound’s finite-size loss is μ ∼ 1/√k, alongside logarithmic security terms.Source: C. Finite-Key Bound · pp. 6–7

Main finite-key bound

• Theorem 6 gives a composable finite-key security bound for BB84, subtracting sampling-corrected noise, error-correction leakage, and verification and privacy-amplification costs from quantum uncertainty.The bound uses preparation quality q and the binary entropy of the error threshold plus the Serfling correction.Source: C. Finite-Key Bound · pp. 6–7

IV. PROTOCOL MODEL

• The protocol layer links what a QKD protocol does to what the security proof certifies, enabling theorems about correctness, secrecy, and abort.The theorem quantifies over every initial state and transcript-dependent adversary channel.Source: §IV · p. 7

A. Syntax

• The finite program language separates classical computation, random sampling, quantum initialization and measurement, and adversarial channel actions.Its syntax can express control flow for prepare-and-measure and entanglement-based protocols.Source: A. Syntax · p. 7
• Atomic constructs include assignments, sampling, quantum initialization and measurement, and Attack[q], alongside sequencing and conditionals.Attack[q] applies an arbitrary adversarial channel to the attacked registers and Eve’s memory.Source: A. Syntax · p. 7
• Fixed-round loops are represented by finite unrolling, with a leading skip making the zero-round loop a well-formed identity map.Protocol listings can relabel the unrolling to number rounds from one.Source: A. Syntax · p. 7

B. Semantics

• A cq-state represents classical memories as a function to possibly sub-normalized quantum states, with normalized states having total trace one.The representation also defines singleton states concentrated at one classical memory.Source: B. Semantics · p. 7
• The adversary chooses a quantum channel based on the public transcript and acts only on attacked registers and its own memory.The adversary can read but not rewrite the public transcript, and security is established over all such actions.Source: B. Semantics · p. 8
• Denotational semantics maps well-formed programs to cq-states, composes sequential commands as function composition, and preserves total mass.Well-formedness requires valid sampling distributions, trace-one initial states, valid measurements, and register separation from adversary memory.Source: B. Semantics · p. 8

C. QKD and BB84

• BB84 uses finite unrolling to a fixed round budget M; insufficient X- or Z-basis matches cause abort, and announcements occur after the loop.The protocol publishes sifting announcements in one step after the loop rather than during quantum rounds.Source: C. QKD and BB84 · p. 8, Figure 2 · p. 9
• The public transcript includes sifting, test, error-correction, verification, and privacy-amplification data, but excludes raw-key subset bit values.The error-correction scheme is fixed before the run and has leakage bounded by leakEC.Source: C. QKD and BB84 · p. 9
• The raw key uses a uniformly chosen size-n subset of X, while parameter estimation computes λ from all detected matching Z-basis rounds.The test uses a cross-multiplied tolerance comparison that remains defined when Z is empty; error correction and privacy amplification are also explicit components.Source: C. QKD and BB84 · pp. 8–9, Figure 2 · p. 9

D. Security Theorem

• The normalized verification-accepted output retains the key, privacy-amplification seed, Eve’s final quantum memory, and remaining public transcript, conditioned on non-abort.It is defined when pabort < 1.Source: D. Security Theorem · p. 9
• The theorem applies to certified source and measurement expressions within the calibrated projective X/Z device class, assuming basis-independent detection and the stated two-universal hashing conditions.Error correction must leak at most leakEC bits, and εc + εs ≤ εtot.Source: D. Security Theorem · p. 9
• For every initial cq-state and adversary strategy, the theorem establishes the protocol’s output-branch behavior, εc-correctness, and εs-secrecy of the accepted output.The theorem concludes combined εtot-security in the stated definitions.Source: D. Security Theorem · p. 9
• Under-sifting, tolerance-test failure, or verification failure produces S = Ŝ = ⊥ as explicit program branches, rather than external theorem premises.The secrecy clause also holds when abort probability is one because its (1 − pabort) prefactor vanishes.Source: D. Security Theorem · p. 9
• With n = k = 104 and the stated BB84 parameters, the instance is εtot-secure for εtot = 3·2^-34 and proves key length ℓ = 2000.The theorem’s key-length bound is at least 2625 for this instance.Source: D. Security Theorem · p. 9

V. PROOF ARCHITECTURE

• The proof decomposes into verified ingredients—the smooth entropic uncertainty relation, Serfling sampling bound, and Quantum Leftover Hash Lemma—which the top-level module composes into security theorems.The architecture follows a single algebraic chain.Source: §V · pp. 9–10

A. Overview

• The utils module supplies quantum primitives, probability infrastructure, and the Serfling bound, while entropy formalizes smooth-entropy calculus and duality.The entropy module includes a first-principles proof of semidefinite-program strong duality used in the LHL proof.Source: A. Overview · p. 10
• The eur and lhl modules formalize the smooth entropic uncertainty relation and Quantum Leftover Hash Lemma, respectively.The uncertainty relation links smooth conditional entropies, and the hash lemma bounds key distance from uniform using smooth min-entropy.Source: A. Overview · p. 10
• The four lower modules are protocol-independent and reusable for other QKD variants and quantum-information or cryptography applications.The qkd layer combines these modules with BB84 security results and a protocol-language instance to close the chain from protocol definition to proof.Source: A. Overview · p. 10

B. Design Features

• Reusable theorem interfaces keep BB84 separate from protocol-independent entropy, uncertainty, hashing, and sampling results, with side conditions stated explicitly.The lower layers quantify over abstract quantum objects and can be instantiated by QKD variants using the same smooth-entropy proof route.Source: B. Design Features · p. 10

A. Backend and Trusted Computing Base

• MATHCOMP supplies algebra, MATHCOMP-ANALYSIS supplies analysis, and COQQ supplies finite-dimensional quantum theory for the development.These libraries provide the mathematical and quantum-mechanical substrate on which FVQKD is built.Source: A. Backend and Trusted Computing Base · p. 11

VI. PROOF ENGINEERING

• The proof infrastructure is built from scratch, with 102,302 lines of fully verified smooth-entropy, purified-distance, smooth-EUR, and Quantum-LHL development.The trusted computing base consists of the Rocq kernel and three standard MATHCOMP-ANALYSIS axioms.Source: A. Backend and Trusted Computing Base · p. 11

B. Representation Choices

• Three representation levels—matrices, typed linear maps, and label-indexed operators—let proofs use convenient abstractions, with coercion lemmas connecting them.The levels progress from direct computation toward textbook notation.Source: B. Representation Choices · p. 11

C. Artifact Summary

• The four upper modules are protocol-independent and account for approximately 68% of the development by lines of code; the qkd module contains the protocol layer.The development contains no Admitted declarations and relies on the Rocq kernel plus three MATHCOMP-ANALYSIS axioms.Source: C. Artifact Summary · p. 11

VII. VERIFICATION FINDINGS

• Mechanization forces side conditions to be stated and discharged, exposing implicit conditions and missing proof branches in published arguments.The verification findings concern both missing branches and competing conventions across the literature.Source: §VII · p. 11

A. Missing Proof Branches

• When parameter-estimation pass probability is too low, rescaling the smoothing parameter can put the EUR outside its domain; FVQKD splits the proof into valid-EUR and high-abort branches.A second explicit conditioning handles error-verification acceptance, transferring the entropy bound or closing secrecy from abort probability while retaining the published key-length formula.Source: A. Missing Proof Branches · pp. 11–12

B. Competing Conventions

• The proof chain uses differing smooth-entropy conventions for smoothing metrics and conditional-entropy witness domains, so FVQKD fixes definitions and bridges differences at theorem boundaries.Its purified-distance convention supports the exact smooth min/max duality used, while the SDP witness form corresponds to allowing sub-normalized conditioning witnesses.Source: B. Competing Conventions · p. 12

VIII. DISCUSSION

• The proof certifies the information-theoretic argument under a published device model, not device-level attacks or implementation side channels; other protocols require a new top layer.The theorem applies once a device model justifies the supplied source and measurement parameters.Source: §VIII · p. 12

IX. CONCLUSION

• FVQKD gives the first end-to-end machine-checked proof of composable finite-key BB84 security at Tomamichel et al.’s tight bound, with zero incomplete proofs and three standard axioms.The checked proof connects the information-theoretic bound to a formal model of protocol execution.Source: §IX · p. 12

APPENDIX A QKD VARIANT PROGRAM SCHEMAS

• The variant schemas use shared command forms for six-state, B92, BBM92, and E91, while leaving protocol-specific states, measurements, and routines as parameters.E91 uses a Bell-test tail and a nonempty-class guard; the sketch omits a finite-statistics correction for that test.Source: Appendix A · p. 17

A. Proof structure and correspondence

• The proof-structure map links bb84_secure to reusable correctness and secrecy boundaries and records dependencies through uncertainty, entropy, fidelity, and convex-analysis results.The text maps Supplementary Theorem 2 to bb84_secret and says bb84_secure combines it with bb84_correct under εc + εs ≤ εtot.Source: A. Proof structure and correspondence · pp. 17–18, Figure 4 · p. 18

B. Paper-to-Rocq correspondence

• The paper-to-Rocq correspondence table maps numbered security and protocol statements to declarations or model premises, including bb84_secure_protocol.The supplied excerpt identifies the protocol-security declaration and a non-vacuous instance.Source: B. Paper-to-Rocq correspondence · p. 18, Table V · p. 18

APPENDIX C TRUSTED SPECIFICATION

• The trusted-specification appendix says readers need trust only the definitions and theorem statements on which the kernel-checked security results depend.It lists the main theorem endpoints alongside their mathematical readings.Source: Appendix C · p. 19, A. Main Theorems · p. 19, 1) Endpoints · p. 19

1) Endpoints:

• The BB84 endpoints formalize both a finite-key security theorem and a protocol-level guarantee for every adversary and well-formed run under stated premises.The finite-key conclusion is Secureεtot; the protocol endpoint also packages abort/pass probabilities, terminal-store branch shape, and ε-security.Source: 1) Endpoints · pp. 20–22

2) Mathematical Closure:

• The mechanization defines seven auxiliary registers for Stinespring dilation, purification, and copies used in data-processing steps.The excerpt introduces the auxiliary-register record but does not provide further register details.Source: 2) Mathematical Closure · p. 22
• The register schemas enforce disjointness and dimension constraints for auxiliary, copy-source, and copy-target registers used in BB84.The copy-source and copy-target registers are specified as disjoint from the key, basis, and Ciso registers and from one another.Source: 2) Mathematical Closure · pp. 22–23
• The protocol record supplies BB84 parameters, while its key-length upper bound subtracts entropy, statistical-correction, error-correction-leakage, and correctness terms.The correction uses a truncated binary entropy evaluated at the tolerance plus the sampling correction.Source: 2) Mathematical Closure · pp. 23–24
• Combined security requires correctness and secrecy, with εc + εs ≤ εtot; secrecy bounds optimized distance from uniform and scales it by the non-abort probability.Correctness is expressed as mismatch probability at most εc; secrecy requires (1 − p_abort) times the distance bound to be at most εs.Source: 2) Mathematical Closure · p. 24
• The hashing definitions formalize collision probability and two-universality, while BB84 verification uses a seed-weighted mismatch probability and an abort/pass relation.For a finite output range of size 2^ℓ, the two-universal collision bound is 2^-ℓ; the numeric side conditions also require nonnegative error-correction leakage and correctness error in (0, 1].Source: 2) Mathematical Closure · p. 25
• The cq-state and post-hash constructors define the joint states used by the privacy-amplification and leftover-hash lemmas.A public-leakage certificate packages a subnormalized positive state classical on the public register, with the original state as its marginal and leakage bounded by the register dimension.Source: 2) Mathematical Closure · pp. 25–26
• The finite-dimensional source certificate supplies the entropic-uncertainty-relation inputs through two POVMs, an overlap-quality condition, and specified measurement dimensions.The side-information dimensions are arbitrary.Source: 2) Mathematical Closure · p. 26
• The utility definitions encode bitstrings and Hamming distance, then specify holdout sampling and error events under a random permutation.The ordinal/bitstring bijection supplies the finite basis-index encoding used in state construction.Source: 2) Mathematical Closure · p. 27

2) Mathematical Closure

• A canonical permutation lists a sampled subset in increasing order before its complement, supporting uniform subset sampling and the sampled-pair error event.The schemas encode sampled and holdout bitstrings through that permutation and define the uniform subset weight using the reciprocal of the number of k-subsets.Source: 2) Mathematical Closure · p. 27
• The BB84 model defines source-weighted pass probabilities and a normalized mixture of holdout-pair states conditioned on the sample error threshold.The schemas specify a full-string source, a pair pass probability, a total pass probability, and the normalized holdout-pair mixture.Source: 2) Mathematical Closure · p. 28
• The measurement schemas define POVM overlap and the corresponding post-measurement states on registers XB and ZC.The overlap is the maximum squared Hilbert–Schmidt norm of the product of the square roots of the POVM elements; the q value is minus its base-2 logarithm.Source: 2) Mathematical Closure · pp. 28–29
• Dimension certificates transport products of disjoint-register dimensions and the source relation nZ = 2n to the corresponding labelled Hilbert-space dimensions.These equalities provide dimension arguments used by the EUR state wrappers and the BB84 holdout-state construction.Source: 2) Mathematical Closure · p. 29
• The delayed-measurement condition certifies a normalized common extension whose partial traces yield the specified states, with labelled-space transports provided for partial traces and bipartite matrices.The appendix also notes that the corresponding Hmax theorem appears in Table VI.Source: 2) Mathematical Closure · p. 30

3) Protocol Closure:

• The command language covers assignments, sampling, quantum initialization and measurement, attacks, conditionals, and sequencing, with fixed loops expanded into sequences.Commands are defined over store-indexed expressions, distributions, states, and measurements.Source: 3) Protocol Closure · pp. 30–31
• BB84’s finite classical-variable layout assigns each round five locations and provides 18 distinct global locations for protocol data.Round locations store Alice’s basis and bit, Bob’s basis and outcome, and a detection flag; global locations include parameters, transcripts, seeds, keys, and abort state.Source: 3) Protocol Closure · p. 31
• The store value type is a disjoint tagged sum covering protocol values from detector outcomes and transcripts to raw and final keys.Distinct injections preserve value distinctions even when payload types coincide.Source: 3) Protocol Closure · p. 31
• Quantum labels distinguish signal, source, and bridge systems, while singleton signal and source labels define round registers and matrix transports embed operands into labelled spaces.The labelled spaces include C2 signal, C4 source, and the bridge Hilbert spaces HE(x) and HB(x).Source: 3) Protocol Closure · p. 34

Protocol Closure

• The bridge uses eight finite registers for the signal, public and key data, test data, flags, and privacy-amplification output.Their dimensions encode the relevant round, key, error-correction, and output-length parameters.Source: 3) Protocol Closure · p. 35
• The denotational semantics models classical-quantum states and command execution, with conditionals selecting branches and sequential commands composed in order.The state invariant requires positivity and unit total mass; adversary channels act on the attacked registers together with the adversary register.Source: 3) Protocol Closure · p. 36
• Each round supports prepare-and-measure or entanglement-based preparation, followed by adversarial distribution, measurement, and sifting.The model also defines X/Z basis encodings and a coherent pointer for the source qubit.Source: 3) Protocol Closure · pp. 35, 37
• Parameter estimation samples key and test rounds, while the program aborts when either sample is too small or the observed error exceeds Qtol.The parameter-estimation, reconciliation, and privacy-amplification components are modeled as protocol commands.Source: 3) Protocol Closure · p. 37
• Error correction publishes reconciliation data, decodes Bob’s key, and verifies matching hashes before privacy amplification hashes both keys to length l.The resulting transcript is extended with the error-correction and privacy-amplification data.Source: 3) Protocol Closure · p. 38
• Concrete adapters decode basis, bit, and outcome values and transport device operations into the labelled signal and source registers for each round.The adapters cover state preparation, measurement, pairing, and pointer operations.Source: 3) Protocol Closure · pp. 38–39
• Finite-sample adapters enumerate selected indices, form key and partial test strings, count disagreements, and represent sample and verification and privacy-amplification seeds as uniform distributions.The sample is uniform over n-subsets of X, and both seed types are uniform over their finite seed spaces.Source: 3) Protocol Closure · p. 39
• Value adapters implement reconciliation, verification, and privacy amplification, append protocol data to the transcript, and project public data as (rounds, K, ZA, ZB, g).The EUR-public projection retains exactly those five components.Source: 3) Protocol Closure · p. 40
• The protocol mode initializes an empty transcript and sets, executes M rounds in prepare-and-measure or entangled mode, then announces rounds and performs parameter estimation.The modes are selected by b = false for PM and b = true for EB.Source: 3) Protocol Closure · pp. 41–42

3) Protocol Closure:

• Parameter estimation can abort the run; otherwise execution proceeds to reconciliation, verification-tag checking, and privacy amplification.The reconciliation step uses certified public reconciliation, decoding, verification-seed, and two-universal verification-hash operations.Source: 3) Protocol Closure · pp. 42–43
• The evaluation definition denotes the BB84 program in the selected entangled mode, adversary, and input state.A separate output construction selects non-abort stores for its state.Source: 3) Protocol Closure · pp. 43, 45
• For the output mode, the final key, privacy-amplification seed, transcript, reconciliation message, and verification tag are reified as computational-basis projectors.The public-register replacement traces out the old public registers and appends their classical reification.Source: 3) Protocol Closure · pp. 44–45
• The certified-device record packages source-overlap and preparation assumptions, complete measurements and pointer readout, basis-independent no-click probability, and classical reconciliation, verification, and privacy-amplification maps.The source dimensions and normalized preparation states are among the stated certificate conditions.Source: 3) Protocol Closure · p. 45

Protocol Closure

• The device class specifies projective Z readout up to the click operator, a standard computational/Hadamard EB pointer, a coherent source-pair purification, and a standard projective source X POVM.The certified-device record also includes the no-click POVM equality assumed by Tomamichel et al..Source: 3) Protocol Closure · pp. 46–47
• A sampled history records each round’s choices and outcomes plus the parameter-estimation subset and verification and privacy-amplification seeds, then determines a classical replay store.The replay begins with an empty transcript and sift sets and a false abort flag, and recomputes sift sets as rounds are written.Source: 3) Protocol Closure · p. 48
• The deterministic replay computes the same classical tail as the sampled program, aborting on failed sifting or parameter estimation or unequal verification tags, and otherwise writing both final keys and the transcript.The tail includes announcement, parameter estimation, reconciliation, verification, and privacy amplification.Source: 3) Protocol Closure · p. 49
• Run abort, pass, and output-mismatch probabilities are defined over the output cq-state, with mismatch requiring unequal keys and no abort.Each probability sums the real trace weight over stores satisfying its event.Source: 3) Protocol Closure · p. 50
• Every terminal store is either an abort with both keys bottom or a non-abort with both keys equal to total privacy-amplification adapter outputs.The branch-shape definition spells out these two cases.Source: 3) Protocol Closure · p. 50
• In the non-abort branch, the two keys are privacy-hash outputs of the final history and the respective secret registers BVXA and BVXhat.The branch stores the hash of sec BVXA as S and the hash of sec BVXhat as Sh.Source: 3) Protocol Closure · p. 50

• The component security theorems come before the reusable foundations and proof pipeline.Source: B. Component Theorems · p. 50

1) Secrecy:

• The secrecy theorem is identified as a theorem of Tomamichel et al.Source: 1) Secrecy · p. 50
• The theorem statement includes a public-leakage set and a two-universal hash family for the key output.Source: 1) Secrecy · p. 50
• The secrecy component theorem extends the source state with a public classical register and splits it into accepted and rejected blocks.Source: 1) Secrecy · p. 50
• The theorem specifies an output state on the key and public registers, with positivity and trace conditions stated for that state.Source: 1) Secrecy · pp. 50–51

Conclusion.

• Under stated parameter and BB84 premises, the theorem concludes secrecy for the output state using an optimized integer key-length bound.The premises include 0 < εc ≤ 1, leakEC ≥ 0, n,k > 0, and 0 < εs ≤ 1; the key-length premise uses ε and ebar with ε + ebar ≤ εs.Source: Conclusion · p. 51

2) Correctness:

• For a nonempty tag set, two-universal verification hash, and bounded mismatch weights, BB84 correctness gives Pr[S̸ = Ŝ ∧ ¬abort] ≤ εc.The theorem requires the inverse tag count to be at most εc.Source: 2) Correctness · p. 51, 1) Definitions · p. 51

1) Definitions:

• The entropy infrastructure proves smooth min/max entropy duality and recovers the unsmoothed entropies at smoothing radius zero for nonzero subnormalized states.The duality statement is in extended-real form and has explicit state and register premises.Source: 1) Definitions · pp. 53–54

2) State Distance:

• Purified distance on subnormalized states satisfies the metric laws, including symmetry, the triangle inequality, and separation.Source: 2) State Distance · p. 54
• The development also establishes bounds relating purified distance to generalized trace distance and trace deficit.Source: 2) State Distance · p. 54
• For completely positive trace-non-increasing channels, purified distance is monotone; finite dilations are isometries for trace-preserving maps and contractions for trace-non-increasing maps.The channel condition packages complete positivity and trace non-increase.Source: 2) State Distance · p. 55
• Purifications and extensions of ρ can be matched by corresponding states for τ at exactly the same purified distance, under the stated subnormalized-state conditions.The extension result encodes the auxiliary purification space with equal-dimension and labelled-register disjointness hypotheses.Source: 2) State Distance · p. 55
• Reusable raw-fidelity laws establish symmetry, CPTP monotonicity and an upper bound, a Uhlmann purification witness, projector identities, Loewner monotonicity, and direct-sum additivity.Direct-sum additivity gives F(ρ1 ⊕ρ2, τ1 ⊕τ2) = F(ρ1, τ1) + F(ρ2, τ2).Source: 2) State Distance · p. 56
• Any nonzero subnormalized state σA with rank σA ≤ b has a rank-one subnormalized purification on A ⊗ Cb.The result provides a reusable finite-dimensional existence theorem.Source: 2) State Distance · p. 56

3) Entropy Calculus:

• For the induced primal and dual SDPs, a finite primal value and strict dual Slater witness imply equal values and primal attainment; min-entropy also has a dual supremum and pointwise weak duality.Every positive semidefinite dual-feasible YAB with TrA YAB ⪯ IB satisfies Tr(ρABYAB) ≤ Φ(ρAB).Source: 3) Entropy Calculus · p. 57
• The min-entropy quantity Φ is positively homogeneous, monotone, subadditive, and convex on positive inputs.The same calculus establishes preservation under local isometries and multiplicativity on tensor-product states.Source: 3) Entropy Calculus · p. 57
• Processing either subsystem cannot increase Φ under the stated map hypotheses, and smooth min- and max-entropies obey generalized data processing for three-register maps.The map on A must be sub-unital CPTN, while the maps on B and C are CPTN for smooth min-entropy and CPTP for smooth max-entropy.Source: 3) Entropy Calculus · pp. 57–60
• Operational min-entropy is characterized by optimizing over channels and, equivalently, their dilations, with min/max duality stated over extended-real spaces.The channel optimization uses CPTP maps, while the dilation characterization uses an isometry and a normalized auxiliary state.Source: 3) Entropy Calculus · pp. 58–59
• For 0 ≤ ε < √Re Tr(ρAB), optimal smooth min- and max-entropy witnesses exist in the product of the two marginal supports.The development also proves smooth max-entropy attainment for normalized sub-states under the same radius condition.Source: 3) Entropy Calculus · p. 59
• For states classical on X, smooth min-entropy after tracing out X is at most the corresponding entropy retaining X, and the latter is bounded below by the former minus log2 dim(X).Both bounds require a subnormalized state and 0 ≤ ε < √Re Tr(ρXAB).Source: 3) Entropy Calculus · p. 60
• The calculus supplies two smoothed min-entropy inequalities and a coherent-copy max-entropy bound under support and positive-trace hypotheses.The coherent-copy inequality bounds the max-entropy on X′B by that on XX′B.Source: 3) Entropy Calculus · pp. 60–61

Definitions.

• Definitions formalize trace-distance smoothing, state-conditioned min/max entropy, optimization over conditioning states, and extended-real/real forms with zero-state laws.The trace ball constrains both the smoothed state’s trace and its trace distance from the original state.Source: Definitions · p. 61
• For orthogonal families and purifier dimension ab ≤ e, coherent-superposition smooth min-entropy is bounded below by labeled-mixture smooth min-entropy minus a classical max-entropy term.The result assumes a positive conditioning state; zero summands are permitted.Source: Definitions · p. 62
• All finite-dimensional smooth extrema are attained for state-conditioned and optimized conditional min/max entropy, given positive semidefinite inputs and nonzero conditioning dimension.The state-conditioned extrema are attained within the trace ball; the optimized forms attain their values over conditioning states.Source: Definitions · p. 62
• Reusable smooth conditional min-entropy laws cover tensor superadditivity, strong subadditivity, classical conditioning, the chain rule, and classical-product data processing.These statements are conjoined in the smooth min-entropy calculus.Source: Definitions · p. 63
• For classical i.i.d. pairs, the library formalizes a classical AEP for nonempty alphabets, positive sample size, and 0 < ε ≤ 1.The probability table is required to be nonnegative and normalized.Source: Definitions · p. 64
• For finite-block classical pairs, normalized smooth max and min conditional entropies are bounded above and below by classical conditional entropy plus or minus δ.Zero-weight pairs contribute zero to the conditional entropy.Source: Definitions · p. 64
• For independent non-identically distributed pairs, the corresponding bounds center on the average single-pair conditional entropy, with the same finite-block correction δ.The theorem extends the finite-block pair bound to independent families.Source: Definitions · p. 64
• For quantum product states, a smooth min-entropy lower bound uses the state’s entropy terms and a correction δ under explicit size and full-rank premises.The stated conditions include n > 0, 0 < ε ≤ 2, and 4 log2(2/ε) ≤ n.Source: Definitions · p. 65
• The cq specialization lower-bounds smooth min-entropy by H(ρ_XB) − H(ρ_B) − δ and states finite-block threshold and rank premises explicitly.The premises include full rank for ρ_B and rank at least two for ρ_X.Source: Definitions · p. 65

1) Measurements:

• The measurement layer defines a two-dimensional X-basis POVM and formalizes POVM overlap and post-measurement states, transporting these states into labelled registers.The X-basis vectors are vx = ((−1)^xz)z and Mx = 1/2 vxv†x.Source: 1) Measurements · pp. 65–66

2) Main Relation:

• The generic uncertainty relation bounds smooth min- plus max-entropy by measurement overlap, while its corollary gives a lower bound of n_key q when n_key q ≤ q(M, N).The states are subnormalized, the measurements are POVMs, and the smoothing parameter satisfies 0 ≤ ε < √Tr ρ.Source: 2) Main Relation · pp. 66–67

3) Entropy Bridges:

• Entropy bridges lift close marginal states to close extensions, with pure extensions when the original state is pure and rank τA ≤ dim B, and establish mixed-state Hmax data processing under purification.The data-processing statement bounds smooth Hmax for the purified extension by smooth Hmax for the original state.Source: 3) Entropy Bridges · p. 67

1) Hash Families:

• Independent composition of δ1- and δ2-almost-two-universal hash families is (δ1 + δ2)-almost two-universal, and seed or input/output relabelings preserve two-universality.The all-functions family achieves collision probability |Z|^-1 for distinct inputs, though its seed is generally exponential in the input description.Source: 1) Hash Families · p. 68

2) Leftover Hash Lemma:

• The smoothed quantum Leftover Hash Lemma bounds distance from uniform by ε plus a square-root term determined by output dimension and smooth conditional min-entropy.Its hypotheses include positivity, sub-normalization, classicality, disjoint registers, two-universality, and ε ≥ 0.Source: 2) Leftover Hash Lemma · p. 68

3) Sampling Bounds:

• For N = n + k, the formalized Serfling bound controls holdout error conditioned on total error, with an unconditional deviation bound also exposed for BB84 sampling.The conditional tail is exp(−2nNδ^2/(k + 1)); the unconditional bound uses the permutation deviation event.Source: 3) Sampling Bounds · p. 69

4) Extractor Lemmas:

• The extractor core formalizes a Schatten-norm Hölder inequality and bounds collision entropy by c Tr ρXE when ρXE ≤ c(1X ⊗ σE), with a normalized σE bound from conditional min-entropy.For subnormalized ρXE, some normalized σE satisfies ΓC(ρXE | σE) ≤ 2^-Hmin(X|E)ρ.Source: 4) Extractor Lemmas · p. 69
• The extractor lemmas provide a normalized adversary state whose support covers the adversary marginal and whose collision entropy is bounded by expR(-hmin E rhoXE * ln 2).The accompanying operator implication relates an operator upper bound to collision entropy.Source: 4) Extractor Lemmas · p. 70
• For a cq-state, an optimal smooth-min witness can remain cq, provided epsilon is below the square root of the state’s trace.The lemma states that the witness lies in the epsilon-ball and attains the smooth-min entropy.Source: 4) Extractor Lemmas · p. 70
• Post-hashing contracts purified distance, while distance from uniform is bounded by the purified distance to an intermediate state plus that state’s distance from uniform.The post-hashing result instantiates the general CPTP contraction theorem.Source: 4) Extractor Lemmas · p. 70

Privacy amplification.

• The almost-two-universal hashing theorem bounds the hashed key’s distance from uniform in terms of smoothing parameters, the collision parameter, output dimension, and smooth min-entropy conditioned on E.Its assumptions include a normalized cq-state, nonnegative delta and epsilon, positive epsilon_bar, and delta-almost-two-universal hashing.Source: Privacy amplification · p. 71

5) Seed Averaging:

• Two-universal and almost-two-universal hashing bound the seed-averaged distance from uniform using the output dimension and conditional min-entropy, with the latter bound depending on δ and ε̄.The formal statements assume a normalized cq state; the almost-universal bound also assumes δ ≥ 0 and ε̄ > 0.Source: 5) Seed Averaging · p. 71

6) Short Seeds:

• δ ≤ (r −1)/2^k + 2^-ℓ for the composed short-seed family, whose theorem exposes positivity, ℓ≤k, register-dimension, and floor-convention conditions.The constructed family also bounds δ by (1 + 4ε^2)/2^ℓ and gives a smooth-min-entropy-based secrecy bound for the hashed state.Source: 6) Short Seeds · pp. 72–73

1) Parameter Estimation:

• ε^2 bounds the weighted mass of passing executions with excessive holdout error, and the conditional deviation probability is at most ε^2/p_pass.The resulting BB84 key smooth max-entropy is bounded by n h_trunc(Qtol + μ), while the total Hamming-ball bound covers δ ≤ 1/2.Source: 1) Parameter Estimation · pp. 73–74

2) Entropy Transfer:

• A CPTP delayed measurement transfers the smooth max-entropy bound from Bob’s quantum register to the measured register; classical public leakage reduces smooth min-entropy by log d_C.The leakage bound also holds using any certified upper bound on the leakage.Source: 2) Entropy Transfer · p. 75
• For states supported on BB84’s good subspace, max-entropy is bounded by n_key times the truncated binary entropy of the tolerated error rate.The bound applies to normalized states with positive key length and positive tolerance.Source: 2) Entropy Transfer · p. 76
• Parameter estimation bounds the pass mixture’s good-subspace mass, enabling smoothing to transfer that mass bound into a smooth max-entropy bound.The smoothing step requires good-subspace mass at least 1 − ε0^2, with 0 ≤ ε0 < 1.Source: 2) Entropy Transfer · p. 76
• Bob’s computational-basis readout uses max-entropy data processing to bound Hε0 max(Z|Bq) by Hε0 max(Z|Z′).The proof models readout as a dephasing map.Source: 2) Entropy Transfer · p. 77

3) Privacy Amplification:

• The Quantum Leftover Hash Lemma bounds hashed-key distance from uniform using the key-length minus smooth-min-entropy gap.Its bound adds ε′ to a square-root term determined by that gap.Source: 3) Privacy Amplification · p. 77
• The leakage rearrangement and key-length premise yield a secrecy bound, which the proof carries through public leakage, accepted-state postselection, and privacy amplification.The resulting distance bound is ε′ + ebar.Source: 3) Privacy Amplification · pp. 77–78

4) Key Length:

• For 0 < εs ≤ 1, the feasible floored key-length set is nonempty and bounded above, and every integer target below its supremum has a concrete parameter witness.The witness supplies positive ε and ebar with ε + ebar ≤ εs.Source: 4) Key Length · p. 78
• When ε^2 < ppass, the smoothing radius lies in the EUR domain; otherwise, the abort/pass relation and secrecy budget bound secrecy without the EUR.In the high-abort branch, 1 − pabort ≤ εs.Source: 4) Key Length · p. 79

1) Well-Formedness:

• Protocol well-formedness requires valid sampling distributions, unit-trace initialized states, complete measurements, and register separation from the adversary workspace.Well-formedness is closed under sequencing and finite loops.Source: 1) Well-Formedness · p. 79

2) Denotation:

• Command denotation is linear and sequential, decomposes over store blocks, and preserves positivity, mass, and well-formedness under the stated well-formedness conditions.Every cq-state decomposes into singleton states, and denotation distributes over those blocks; well-formed commands preserve positive semidefinite blocks and cq-mass.Source: 2) Denotation · pp. 79–80

3) Classical Transport:

• A generic noninterference-style lemma transports per-round partial-trace equality through classical commands, including announcements, estimation, error correction, abort branches, and privacy amplification.The condition excludes initialization, measurement, and adversarial quantum actions; equality must hold initially for every store block.Source: 3) Classical Transport · p. 80

1) Source and Device:

• The BB84 instance supplies concrete qubit preparation and measurement, a certified full-string source, and a coherent entangled pair with Alice’s basis-dependent pointer.The adapters certify dA = dX = 2n, a nonzero Bob register, and the standard-Z overlap lower bound; the X and Z preparations use projective states and the outcome-None operator is zero.Source: 1) Source and Device · pp. 81–82

2) Classical Components:

• The classical instance uses zero-bit reconciliation and two two-universal field-hash families for verification and privacy amplification.For r = 34 and 2000, the verification and PA families have 2n seeds and 2^34 tags or 2^2000 outputs, respectively; decoding returns Bob’s string unchanged.Source: 2) Classical Components · p. 82
• The classical instantiation uses two-universal hashing for verification and privacy amplification, with positive seed counts for both maps.The verification and privacy-amplification maps are built from finite-field hashes.Source: 2) Classical Components · p. 83

3) Device Package:

• The shipped device is a prepare-and-measure specialization with a projective X/Z certificate, and its liveness witness uses the identity attack.The concrete certificate fixes q = 1 and the prepare-and-measure source flag.Source: 3) Device Package · p. 84, 4) Run Witness · p. 85

4) Run Witness:

• A generic reachability theorem proves p_pass > 0 for histories satisfying positive trace, detected-round, key/test-set, zero-bit, and positive-weight conditions.The concrete identity-adversary witness discharges those premises separately.Source: 4) Run Witness · pp. 85–86

5) Result:

• With fixed round budget M = 2,000,000, the checked fixed-parameter expression is at least 2625, and its optimized witness proves the 2000-bit key-length premise for each admissible ec.Source: 5) Result · p. 86
• For each source mode, Theorem 11 combines positive pass probability for an explicit witness with security for every adversary and well-formed initial state.The theorem also gives p_abort + p_pass = 1 and bounds output mismatch by bb84_eps_c, with eps-secure error at most bb84_eps_c + ex_eps_s.Source: 5) Result · p. 87