# Quantum Cryptography and Autoformalization in Lean

> This paper delivers the first end-to-end machine-verified security proof of qubit BB84 QKD against coherent attacks, formalized in Lean 4 with a tighter entropy bound.

- **Source:** [arXiv](https://arxiv.org/abs/2610.17286)
- **Published:** 2026-10-17
- **Permalink:** https://picx.dev/p/3MJoyP
- **Whiteboard:** https://picx.dev/p/3MJoyP/image

## Summary

# 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

| Quantity | Previous Bound | New Bound | Improvement |
|----------|---------------|-----------|-------------|
| Variance cap for binary key | $\log_2^2(5) \approx 5.39$ bits² | $\log_2^2(1+\sqrt{2}) \approx 1.62$ bits² | ~3.3× reduction |
| General variance bound | $\log_2^2(2d_W + 1)$ | $\log_2^2(\sqrt{d_W} + \sqrt{d_W-1})$ | ~4× for large $d_W$ |

## 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

---

_Markdown view of https://picx.dev/p/3MJoyP, served by PicX — AI-generated visual whiteboard summaries of research papers._