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

AI summary

Overview

Research area: Quantum cryptography and formal verification — specifically the machine-checked verification, in the Rocq proof assistant, of the security proof for quantum key distribution (QKD).

Technical level: Advanced. The paper assumes familiarity with quantum information theory (density matrices, smooth min- and max-entropy, trace distance), with proof-assistant engineering in Rocq/Coq, and with the standard BB84 security argument. The prose is unusually clear for the genre, but the content is specialist.

Scope (one sentence): The paper presents FVQKD, a reusable Rocq library that delivers, to the authors' knowledge, the first complete end-to-end machine-checked proof of composable finite-key security for BB84, following the tight analysis of Tomamichel et al.

What This Paper Is About

QKD derives key secrecy from quantum mechanics rather than computational hardness, but its security guarantees rest on long, technically delicate pen-and-paper proofs combining results from quantum information theory, cryptography, and physics. The authors build a Rocq library that machine-checks the entire chain from a formal protocol program down to a composable finite-key secrecy statement, so that the guarantee rests both on physical principles and on a kernel-checked proof free of human reasoning errors.

Key Contributions

1. A reusable, protocol-agnostic verification framework. FVQKD machine-checks Uhlmann's fidelity theorem, generalized (sub-normalized) fidelity, purified distance as a metric with monotonicity under completely positive trace-nonincreasing (CPTN) maps, the smooth-entropy calculus (smooth conditional min- and max-entropy, their duality, and classical chain rules), the POVM-general smooth entropic uncertainty relation, the Quantum Leftover Hash Lemma, Serfling's sampling bound, and semidefinite-programming strong duality (the primal direction of Tomamichel's Theorem 2.6, proved from first principles). The majority of the project has no dependence on BB84 or any particular protocol.

2. An end-to-end machine-checked QKD security proof, instantiated for BB84. The development gives an unbroken, kernel-checked chain from a formal protocol program to a composable finite-key ε-security statement at the tight bound of Tomamichel et al. The proof contains no incomplete lemmas and relies only on the Rocq kernel plus three standard axioms inherited from MathComp-Analysis.

3. A formal protocol semantics that grounds the information-theoretic bound. A small programming language models the five BB84 stages, with atomic constructs for classical assignment, random sampling, quantum initialization, measurement, and an adversarial channel action (Attack). This lets the theorem quantify over every initial state and every transcript-dependent adversary channel — something the pen-and-paper analysis does not do.

4. Documented verification findings. The mechanization surfaces necessary side conditions the published argument leaves unstated, one of which reveals a missing proof branch, and it reconciles conflicting conventions across the six theoretical works underlying the BB84 proof.

Main Findings

• First end-to-end formal verification of a QKD security proof. The authors state this is, to their knowledge, the first complete machine-checked proof of composable finite-key security for a QKD protocol. Table I compares FVQKD against prior formal-methods work on QKD (Kubota et al., Boender et al./Kammüller, a Lean project, CryptHOL constructions, CHSH rigidity/Tsirelson formalizations) on five criteria — unbounded quantum adversary, composable security, finite-key bound, explicit protocol model, and end-to-end proof — and reports FVQKD as the only entry meeting all five.

• A missing proof branch was found. The published argument omits side conditions that the mechanization shows are necessary; one of these reveals a missing proof branch in the existing proof.

• Convention conflicts across six works. The formalization had to reconcile differing conventions from the six theoretical works underlying the BB84 security proof before a single chain of lemmas could be composed.

• A domain condition surfaces explicitly. Smooth entropies require 0 ≤ ε < sqrt(Tr ρ); this condition, implicit in informal presentations, becomes a visible obligation in the mechanization.

• The final bound proved. Theorem 6 gives ε_c-correctness, and ε_s-secrecy whenever ℓ ≤ n(q − h(Q_tol + μ)) − leak_EC − log₂(2/(ε_s² ε_c)), where μ = sqrt((n+k)(k+1)/(n k²) · ln(2/ε_s)) is the Serfling correction and h is the binary entropy, truncated to h(x) = 1 for x > 1/2. The bound specializes the optimized bound in Theorem 10 to ε = ε̄ = ε_s/2.

• Explicit trust boundary. Six conditions (T1–T6) are surfaced at different layers: side-channel freedom; authenticated classical channel; source characterization by preparation quality q; delayed measurement; basis-independent detection; and a calibrated projective X/Z class at the executable endpoint. T3 becomes an explicit device-characterization obligation, T2 is fixed by the modeled read-only classical channel, and T5/T6 are device obligations at the executable endpoint while the T4 entropy comparison is proved within that class.

• Only three axioms, no admits. The trusted base is the Rocq kernel plus three standard axioms from MathComp-Analysis; the development is admit-free.

• Reusable across protocol variants. Because BB84, decoy-state variants, and measurement-device-independent protocols in the smooth-entropy tradition share the same chain of entropic uncertainty relation, Quantum Leftover Hash Lemma, and sampling bounds, formalizing the chain once provides a foundation for their future mechanization.

Methodology in Plain English

The authors did not invent a new security proof; they took an existing, well-regarded tight finite-key analysis (Tomamichel et al.) and rebuilt it inside a proof assistant, from the ground up.

The work splits into layers. At the bottom, they build quantum-information infrastructure on top of existing libraries: MathComp for algebra, MathComp-Analysis for real analysis, and CoqQ for finite-dimensional quantum theory. This layer supplies fidelity, purified distance, smooth entropies, and the sampling and hashing lemmas. Above it sits the security argument itself: the entropic uncertainty relation bounds Eve's knowledge of the raw key, Serfling's bound converts the observed error rate on the test block into a bound on the unobserved key block, and the Quantum Leftover Hash Lemma converts the remaining uncertainty into a secret key. At the top, a small formal programming language describes what the protocol actually does — prepare, measure, sift, estimate, correct, amplify — so that the mathematical bound is attached to a concrete executable specification rather than to an abstract state.

Because every step must typecheck, anything the informal proof glossed over becomes a visible obligation: domain conditions on the smoothing parameter, side conditions on the sampling argument, and mismatched conventions between the source papers. That is how the missing proof branch and the unstated conditions were discovered.

Why This Matters

Impact on research. QKD is moving into standardization and commercial deployment, but its guarantees rest on hand-checked proofs of considerable sophistication. Serious gaps in quantum information theory results have been found years after publication, and a recent survey identifies gaps and limitations in published decoy-state BB84 security proofs. FVQKD supplies a second, independent assurance layer: unconditional security from physics, plus machine-checked correctness of the reasoning. It also produces a reusable quantum-information library, so future QKD variants need not re-derive the underlying mathematics.

Real-world applications:

• Deployed QKD links and networks. Commercial and metropolitan QKD systems can point to a kernel-checked finite-key bound when making security claims.
• Satellite-to-ground key exchange. The paper cites the Micius satellite demonstration as evidence QKD has left the laboratory; such links operate at exactly the small block sizes (the paper mentions block sizes as few as 10⁴ quantum signals) where finite-key effects dominate.
• One-time-pad encryption. Composable security is what licenses using the extracted key inside a larger protocol, such as a one-time pad; the mechanized definition is explicitly the composable trace-distance criterion.
• Standards and certification. With QKD under active standardization, a machine-checked reference proof gives standards bodies and evaluators a precise artifact to compare implementations and claims against.

Industry relevance. The work targets the assurance gap that matters for vendors, evaluators, and operators: not whether the protocol is described correctly, but whether the claimed key rate and error tolerance are actually justified. Its explicit trust boundary (T1–T6) also tells implementers exactly which device assumptions — side-channel freedom, basis-independent detection, calibrated sources — the bound depends on.

Future Directions

• Mechanizing decoy-state BB84. Weak-coherent-pulse sources require decoy-state techniques and are explicitly outside the current scope; the shared proof chain is positioned as the foundation for that extension.
• Measurement-device-independent and twin-field protocols. MDI protocols, which remove the need to trust detectors, are named as sharing the same entropic-uncertainty / leftover-hash / sampling structure and are natural next instantiations.
• Discharging the device obligations. T5 and T6 are device obligations at the executable endpoint, and T3 is an explicit characterization obligation; extending the verified class beyond the calibrated projective X/Z model, or connecting it to physical device models, remains open.
• Authentication costs and further protocol families. The proof treats authentication as a primitive and does not model the key it consumes, and the syntax is designed to express prepare-and-measure and entanglement-based protocols such as six-state, B92, BBM92, and E91 — all left as instantiations for future work.

Target Audience

Researchers in quantum cryptography and quantum information theory who want assurance that finite-key BB84 security proofs are sound; formal-methods and proof-assistant researchers interested in quantum cryptography and in large-scale mechanized probability and entropy arguments in Rocq; standards bodies and certification evaluators working on QKD; and graduate students in either area who want a worked example of how deep quantum-information mathematics is reconstructed from first principles in a proof assistant. Readers without background in smooth entropies or dependent-type proof assistants will find the technical sections demanding.

Authors’ abstract

Quantum key distribution (QKD), whose security is derived from quantum mechanics rather than computational assumptions, is moving into standardization and commercial deployment. Yet its security guarantees rest on technically delicate proofs checked by hand. Formal verification closes this gap, establishing a two-factor assurance: unconditional security from physical principles, and machine-checked proofs against reasoning errors. We present FVQKD, a Rocq library for machine-checking QKD security proofs. Its first result is a complete, end-to-end machine-checked proof of composable, finite-key security for BB84. The mechanization reconstructs the complete proof infrastructure from first principles, including the smooth entropy framework, the entropic uncertainty relation, and the Quantum Leftover Hash Lemma. It uncovers necessary side conditions that the published argument leaves unstated, one of which reveals a missing proof branch, and it grounds the information-theoretic bound in a formal semantics of protocol execution, which the pen-and-paper analysis lacks. The proof is entirely admit-free, relying only on the Rocq kernel and standard foundational axioms. To our knowledge, this is the first end-to-end formal verification of a QKD security proof. Built on MathComp, MathComp-Analysis, and CoqQ, the development provides quantum-information infrastructure designed for reuse across broader QKD variants and quantum cryptography applications.