Quantum Cryptography and Autoformalization in Lean

Summary (Overview)

• First end-to-end machine-verified security proof of entanglement-based qubit BB84 quantum key distribution (QKD) against coherent attacks, formalized in the Lean 4 proof assistant.
• LOCC-enforcing protocol language: A typed programming language defined in Lean that enforces local operations and classical communication (LOCC) by construction, eliminating hidden assumptions about protocol implementability.
• Improved conditional-entropy variance bound: A tighter bound on the conditional-entropy variance of classical-quantum states, $V(W|B)_\rho \leq \log_2^2(\sqrt{d_W} + \sqrt{d_W - 1})$, improving on the prior $\log_2^2(2d_W + 1)$ bound, reducing the finite-size penalty in key length.
• LLM-based autoformalization pipeline: The proof was developed through iterative collaboration between researchers and LLM agents (Claude, GPT, and open-weight GLM-5.3-Flash), with the Lean kernel type-checking all derivations.
• Open-source quantum information library: The underlying Lean 4 library (QCryptLean) is released as open source, providing reusable definitions for states, channels, entropies, and LOCC protocols.

Introduction and Theoretical Foundation

Background and Motivation

Quantum key distribution (QKD) aims to establish shared secret keys for private communication, with security derived from quantum theory under explicit device assumptions and authenticated classical communication. A central advance has been composable security, which formalizes when a generated key can safely replace an ideal secret key in subsequent cryptographic applications.

The paper addresses a critical gap in the field: security proofs across quantum cryptography can contain gaps, often between individually valid theorems integrated under mismatched assumptions. For example:

• Nahar et al. closed a gap first identified by Belzig in the application of postselection to QKD
• A comprehensive review documented gaps in security proofs for practical decoy-state BB84 implementations
• Incompatible assumptions arise when combining results from different papers

Theoretical Foundation

The work builds on several key theoretical pillars:

1. Composable security framework [4, 5]: Security is defined via the diamond norm distance between real and ideal channels
2. Postselection technique [8]: Extends security against collective attacks to coherent attacks
3. BB84 phase-error analysis [29, 30]: Relates security to phase-error rate estimation
4. Finite-size entropy bounds [31, 32]: Quantify the gap between asymptotic and finite-key rates
5. Leftover hash lemma: Enables privacy amplification

Prior Formal Verification Efforts

Previous formal methods in quantum information include:

• Process calculi, Coq, and model checking for BB84 verification
• Model-checking of finite, noiseless instances under intercept-resend attacks
• Verification of protocol-equivalence steps in the Shor-Preskill proof
• Formalization of a lemma in the Lo-Chau argument

However, none of these works gives an end-to-end composable finite-key security bound against general attacks.

Methodology

The AI Proving Pipeline

The formalization was developed through iterative collaboration between researchers and LLM agents:

1. Agents (Claude and GPT) translated statements from target papers into Lean
2. Type-checking feedback from the Lean compiler guided the process
3. Numerical checks were used to search for counterexamples or test proposed bounds
4. A loopy sequencer launched agents with task-specific context, including dependency graphs
5. A locally hosted GLM-5.3-Flash model worked on proving tasks set by Claude and reviewed by Claude and GPT

The LOCC Program Language

The paper defines a type called Program whose inhabitants can only be constructed by composing local actions, potentially dependent on public classical communications.

Multipartite system definition:

$$\Gamma = (\Gamma_i)_{i:P}, \qquad \mathcal{H}_\Gamma = \bigotimes_{i:P} \mathbb{C}^{\Gamma_i} \tag{1}$$

Instrument definition (for party $i$, with outcome set $\mathcal{X}$ and Kraus index sets $\mathcal{R}_x$):

$$K_{x,r}: \mathcal{H}_i \longrightarrow \mathcal{H}_i', \qquad x: \mathcal{X}, \quad r: \mathcal{R}_x$$ $$\sum_{x:\mathcal{X}} \sum_{r:\mathcal{R}_x} K_{x,r}^\dagger K_{x,r} = \mathbb{1}_{\mathcal{H}_i} \tag{2}$$

Program constructors:

$$\text{done}, \quad \text{priv}(V, q), \quad \text{announced}(A, y \mapsto q_y) \tag{6}$$

where $V$ is a private action and $A$ is an announced action with report function $g: \mathcal{X} \to \mathcal{Y}$.

Security Definitions

Real channel: $\mathcal{E}^{\text{real}} := p.\text{denote}$ (Eq. 10)

Ideal channel: $\mathcal{E}^{\text{ideal}} := \mathcal{R} \circ \mathcal{E}^{\text{real}}$ (Eq. 11)

where $\mathcal{R}$ erases real keys and writes fresh uniform random strings.

$\varepsilon$-security (diamond norm):

$$\frac{1}{2}\|\mathcal{E}^{\text{real}} - \mathcal{E}^{\text{ideal}}\|_\diamond \leq \varepsilon \tag{12}$$

Robustness (abort probability):

$$p_{\text{abort}}(\rho) \leq \delta_{\text{rob}} \tag{15}$$

BB84 Protocol Construction

The protocol proceeds as follows:

1. Measurement: Alice and Bob measure $N$ qubit pairs in either $Z$ or $X$ basis with instrument:

$$K_{\theta,x}^p = \sqrt{p(\theta)}|\theta, x\rangle\langle\phi_x^\theta| \tag{16}$$

2. Basis announcement and sifting: Parties announce basis strings; Alice announces a random permutation; rounds are partitioned into raw key ($n_K$), $Z$ test ($m_Z$), and $X$ test ($m_X$) blocks with $n := n_K + m_Z + m_X$ (Eq. 17)
3. Parameter estimation: Test round bits are announced
4. Error correction and verification: Syndrome $S(x)$ and verification tag are exchanged
5. Privacy amplification: Final key is a hash of the raw key

Empirical Validation / Results

Theorem 1: Finite-Key Security of BB84

$$\frac{1}{2}\|\mathcal{E}_{\text{BB84}}^{\text{real}} - \mathcal{E}_{\text{BB84}}^{\text{ideal}}\|_\diamond \leq \varepsilon_{\text{QKD}} \tag{18}$$

where:

$$\varepsilon_{\text{QKD}} := \varepsilon_{\text{EV}} + g_{n,4}(\varepsilon_{\text{PA}} + 2\bar{\varepsilon} + 2\sqrt{2\varepsilon_{\text{AT}}}) \tag{19}$$

with $g_{n,4} := \binom{n+3}{3}$ the postselection prefactor, and:

$$\varepsilon_{\text{AT}} := \exp[-m_X \text{kl}(Q + \delta \| Q + \delta + \delta')], \quad \varepsilon_{\text{EV}} := 2^{-\ell_{\text{EV}}} \tag{20}$$

Key length condition:

$$\ell \leq n_K[1 - h_2(Q + \delta + \delta')] - \ell_{\text{EC}} - \ell_{\text{EV}} - 2\log_2 g_{n,4} - P_\beta(n_K, \bar{\varepsilon}) - 2\log_2(1/\varepsilon_{\text{PA}}) + 2 \tag{22}$$

Finite-size penalty:

$$P_\beta(n_K, \bar{\varepsilon}) := \frac{C_\star \ln 2}{2} n_K \beta + K_\beta n_K \beta^2 + \frac{b(\bar{\varepsilon})}{\beta} \tag{23}$$

with $C_\star := \log_2^2(1 + \sqrt{2}) \approx 1.6168$ (bits squared).

Theorem 2: Robustness of BB84

For a memoryless honest channel with QBER $q$:

$$p_{\text{abort}}(\sigma^{\otimes N}) \leq \varepsilon_{\text{quota}} + \varepsilon_{\text{test}} + \varepsilon_{\text{EC}} \tag{25}$$

Theorem 3: Improved Conditional-Entropy Variance Bound

$$V(W|B)_\rho \leq \log_2^2(\sqrt{d_W} + \sqrt{d_W - 1}) \tag{28}$$

This improves the bound $\log_2^2(2d_W + 1)$ of Ref. [32] for every $d_W$. For a binary key:

$$V(W|B)_\rho \leq C_\star = \log_2^2(1 + \sqrt{2}) \approx 1.6168 \tag{29}$$

compared to $\log_2^2 5 \approx 5.39$ from the previous bound.

Key Results Comparison

Theoretical and Practical Implications

Formal Verification Contributions

1. Hidden assumptions made explicit: The formalization revealed implicit assumptions in existing proofs, including:

   • The postselection theorem requires maps to preserve Hermiticity
   • The continuity bound of Ref. [32] requires support containment conditions

2. Reproducible standard: The work sets a reproducible standard for security arguments in quantum cryptography, where the Lean kernel type-checks every derivation.

3. LLM-assisted discovery: The pipeline served as a discovery machine, finding a tighter variance bound that reduces the finite-size penalty on the key rate.

Practical Impact

• Key rate improvement: The improved variance bound reduces the finite-size penalty, enabling shorter raw key blocks for the same security level
• Reusable library: The QCryptLean library provides reusable components including:
  • Quantum leftover hashing with public seed retention
  • Smooth-entropy bounds for classical-quantum tensor-power states
  • Postselection reduction
• Beyond QKD: The protocol language supports any finite set of parties, enabling applications to secure computation, digital signatures, and multiparty deep learning

Conclusion

Main Takeaways

1. First end-to-end machine-verified composable finite-key security proof for entanglement-based qubit BB84 against coherent attacks, built only on Lean's standard axioms (propext, Classical.choice, Quot.sound).

2. LOCC enforcement by construction eliminates an entire class of hidden assumption errors, as demonstrated by the earlier AI-generated protocol error that motivated this design.

3. LLM-based autoformalization proved effective for both verification and discovery, with open-weight models (GLM-5.3-Flash) contributing to key theorems.

4. Tighter mathematical bounds emerged from the formalization process itself, showing that formal methods can accelerate discovery, not just verification.

Future Directions

• Extended protocol types: Represent prepare-and-measure protocols directly by extending the language to describe quantum transmission followed by LOCC processing
• Decoy-state QKD: Formal security proofs for optical QKD with decoy states require suitable source, loss, and detector models
• Alternative security frameworks: Support for entropy accumulation or uncertainty relation-based proofs
• Open-weight model development: Further development of theorem proving with open-weight models through well-tuned harnesses and reinforcement learning