Quantum information · Theory with formal verification
FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq
arXiv:2610.30645v1 ↗PDF ↗Submitted 22 October 2026
- Question
- QKD security rests on hand-checked proofs that chain smooth entropies, an entropic uncertainty relation, a sampling bound and the leftover hash lemma, drawn from several papers with differing conventions. Can the composable finite-key security of BB84 be machine-checked end to end, from a formal protocol program to the key-length theorem?
- Result
- Yes, in FVQKD, a Rocq development of about 151,000 lines, 102,000 of them new, with no admitted lemmas and only the kernel plus three standard axioms. It proves composable finite-key security of BB84 at the tight Tomamichel et al. bound, for every initial state and every adversary channel acting on a formally specified protocol program. Mechanization exposed a missing case in the published argument: after conditioning on the test passing, the smoothing parameter \(\varepsilon/\sqrt{p_{\rm pass}}\) can exceed 1, outside the domain of the uncertainty relation. A second proof branch using the abort probability repairs it, and the key-length formula is unchanged. A concrete instance with \(n=k=10^4\) certifies a 2000-bit key.
The paper in detail
In BB84, sifting leaves \(n\) key rounds and \(k\) test rounds. The protocol aborts if the test error rate exceeds \(Q_{\rm tol}\), reconciles keys while leaking \(\mathrm{leak}_{\rm EC}\) bits, checks agreement with a hash, and compresses the key by two-universal hashing. Security means \(\varepsilon_c\)-correctness and \(\varepsilon_s\)-secrecy, \((1-p_{\rm abort})\min_\sigma\tfrac12\|\rho_{SE}-\tau_S\otimes\sigma_E\|_1\le\varepsilon_s\), which is composable. The target bound is \(\ell\le n(q-h(Q_{\rm tol}+\mu))-\mathrm{leak}_{\rm EC}-\log_2\tfrac{2}{\varepsilon_s^2\varepsilon_c}\), where \(\mu\sim1/\sqrt k\) is the only finite-size loss beyond logarithmic terms.
The development has five modules in dependency order, \(\texttt{utils}<\texttt{entropy}<\{\texttt{lhl},\texttt{eur}\}<\texttt{qkd}\), built on MathComp, MathComp-Analysis and CoqQ. The lower four contain no protocol-specific content. They include Uhlmann’s theorem, purified distance with monotonicity under trace-nonincreasing maps, smooth min- and max-entropies and their duality, the POVM-general smooth uncertainty relation, the quantum leftover hash lemma, Serfling’s bound, and what the authors describe as the first machine-checked SDP strong-duality theorem. The top layer composes them as sealed theorems.
A small command language with classical and quantum variables, sampling, measurement and an adversary channel action gives the protocol a formal semantics on classical–quantum states. Sifting, parameter estimation and verification become program branches ending in \(\perp\). Theorem 10 quantifies over every initial state and every transcript-dependent adversary. Six trust assumptions, such as no side channels, an authenticated classical channel and a characterized source, appear as explicit hypotheses or device obligations. For \(n=k=10^4\), \(Q_{\rm tol}=1\%\), \(\mathrm{leak}_{\rm EC}=1024\) and \(\varepsilon\) parameters \(2^{-34}\), the artifact proves the key-length expression is at least 2625 bits, certifying \(\ell=2000\) at \(\varepsilon_{\rm tot}=3\cdot2^{-34}\).
Two side conditions were missing from the published proof. Smooth entropies need \(\varepsilon<\sqrt{\operatorname{Tr}\rho}\). Conditioning on the test passing rescales \(\varepsilon\) to \(\varepsilon/\sqrt{p_{\rm pass}}\), which an adversary forcing aborts can push above 1: \(p_{\rm pass}=10^{-12}\) and \(\varepsilon=10^{-5}\) give 10. The key is also conditioned on verification accepting, a second event the published proof does not treat. Beyond these gaps, the six source papers define smoothing balls by purified distance or by a generalized trace distance, and optimize over normalized or sub-normalized witnesses. The duality \(H^\varepsilon_{\max}(A|B)=-H^\varepsilon_{\min}(A|C)\) relies on purified distance, so FVQKD fixes one convention and bridges the others with coercion lemmas.
Transferable methods
The finite-key bound as a chain of entropy inequalities
The key-length theorem is assembled from three independent results. The uncertainty relation converts Bob’s correlation with Alice into Eve’s ignorance, the sampling bound controls the unobserved error rate, and the leftover hash lemma turns min-entropy into a nearly uniform key. Each is a separately verified module.
The uncertainty relation states \(H^\varepsilon_{\min}(X|E)+H^\varepsilon_{\max}(Z|B)\ge nq\), with \(q=-\log_2\max_{x,z}\|\sqrt{M_x}\sqrt{N_z}\|_\infty^2\), and \(q=1\) for conjugate qubit bases. Data processing gives \(H^\varepsilon_{\max}(Z|B)\le H^\varepsilon_{\max}(Z|Z')\), and Serfling’s bound on sampling without replacement gives \(H^\varepsilon_{\max}(Z|Z')\le n\,h(Q_{\rm tol}+\mu)\). Hence \(H^\varepsilon_{\min}(X|E)\ge n(q-h(Q_{\rm tol}+\mu))\).
The chain rule subtracts the \(\mathrm{leak}_{\rm EC}+\lceil\log_2(1/\varepsilon_c)\rceil\) disclosed bits. The leftover hash lemma bounds the distance from uniform by \(\varepsilon+\tfrac12\sqrt{2^{\ell-m}}\), and requiring \(\tfrac12\sqrt{2^{\ell-m}}\le\bar\varepsilon\) gives \(\ell\le m-2\log_2\tfrac1{2\bar\varepsilon}\), the form in Theorem 10.
Editorial check: evaluating the Theorem 10 expression at the instance parameters (\(q=1\), \(\varepsilon=\bar\varepsilon=\varepsilon_c=2^{-34}\)) gives \(\mu=0.0687\), \(h(0.0787)=0.397\) and a right-hand side of about 4900 bits. The artifact proves the weaker lower bound 2625, which is enough to certify \(\ell=2000\).
How to reuse it
Protocols on the smooth-entropy route (decoy-state BB84, six-state, qudit or MDI variants) reuse the same three-part chain. What changes is the uncertainty relation’s overlap \(q\) and the parameter-estimation statistics. Writing a new proof in this form shows exactly which part must be re-proved.
Split on the event probability when conditioning inflates a smoothing parameter
Conditioning on an event of probability \(p\) renormalizes the state and inflates any purified-distance radius by \(1/\sqrt p\). If \(p\) is small the radius leaves the domain where smooth entropies are defined. The fix is a case split: either \(p\) is large enough to apply the theorem, or it is so small that the composable definition’s prefactor makes secrecy trivial.
Smooth entropies require \(0\le\varepsilon<\sqrt{\operatorname{Tr}\rho}\). For the normalized conditional state this means \(\varepsilon'=\varepsilon/\sqrt{p_{\rm pass}}<1\), that is \(p_{\rm pass}>\varepsilon^2\). The published proof checks only \(\varepsilon'\ge0\).
Editorial reconstruction of the second branch: the trace distance is at most 1, so the secrecy quantity is at most \(1-p_{\rm abort}\le p_{\rm pass}\). If \(p_{\rm pass}\le\varepsilon^2\) and \(\varepsilon\le\varepsilon_s\le1\), it is at most \(\varepsilon^2\le\varepsilon_s\). FVQKD applies the same split to the later conditioning on verification acceptance.
How to reuse it
Whenever a proof conditions on a passing test and then applies an \(\varepsilon\)-dependent or smoothed bound (finite-key QKD, randomness certification, device-independent protocols), check the rescaled parameter’s domain. The usual repair is a case split on the event probability, using the \((1-p_{\rm abort})\) factor in the security definition.
Context & limitations
Why it matters. This is the first end-to-end machine-checked QKD security proof. About two thirds of the code is protocol independent: purified distance, smooth-entropy duality, the uncertainty relation, the quantum leftover hash lemma, Serfling’s bound and SDP strong duality. Decoy-state and measurement-device-independent proofs on the same route can reuse it, which matters for certification.
Limitations. Only the information-theoretic argument is verified. Side channels and device imperfections are assumed away, and the executable endpoint is restricted to ideal projective \(X/Z\) devices with basis-independent detection. Weak-coherent sources, decoy states and the key consumed by authentication are not modelled. Device-independent and continuous-variable QKD need new libraries. The finding is a gap in a proof, not an attack.