Quantum Cryptography and Autoformalization in Lean

技术摘要：量子密码学与 Lean 中的自动形式化

问题陈述
量子密钥分发（QKD）依赖于物理原理和数学推理来建立安全通信。然而，该领域的安全性证明经常存在漏洞，特别是在将基于不同假设推导出的独立有效定理进行整合时。近期的综述强调了在实际的诱骗态（decoy-state）实现中，针对 Bennett–Brassard 1984 (BB84) 协议存在的逻辑不一致性，即结合来自不同论文的结果时会引入不兼容的假设。此外，现有的量子信息形式化验证工作主要集中在特定的协议步骤、电路等效性或有限无噪声实例上，未能提供端到端的、机器验证的、针对通用相干攻击的可组合有限密钥安全性界限。

方法论
作者使用 Lean 4 证明助手，开发了一个针对基于纠缠的量子比特 BB84 协议的端到端安全性证明。该方法依赖于一种结合了大语言模型（LLM）与形式化验证的新型流水线：

1. 自动形式化流水线： 研究人员与 LLM 智能体（基于 Claude、GPT 以及本地托管的 GLM-5.3-Flash 模型）进行迭代协作，将目标论文中的非形式化数学陈述转化为 Lean 代码。这些智能体将证明分解为中间命题，利用 Mathlib 库进行可重用的定义，并在尝试形式化证明之前，利用数值检查来搜索反例。
2. LOCC 协议语言： 为了确保对协议的忠实表示，作者在 Lean 中定义了一种自定义类型 Program，通过构造方式强制执行局部操作与经典通信（LOCC）。该语言将 Alice 和 Bob 的操作建模为作用于局部寄存器的 Kraus 映射，并明确记录了公开公告。这种结构通过将局部性和公开通信设为显式约束，防止了逻辑错误（例如假设参与者拥有他们并不拥有的密钥）。
3. 形式化验证： Lean 内核根据其定理陈述和声明的公理（特别是 propext、Classical.choice 和 Quot.sound）对每个证明项进行类型检查。作者的审查重点在于验证形式化定义和定理陈述是否准确反映了预期的物理协议和安全性主张，而非重新验证其证明逻辑本身。

核心贡献

• 首个端到端机器验证证明： 本文展示了第一个针对相干攻击的、经过机器验证的基于纠缠的量子比特 BB84 协议的可组合有限密钥安全性证明。
• LOCC 协议语言： 一种在 Lean 中构建的新型形式化语言，将协议构建为局部动作和公开公告的分支树，确保安全性定义（安全性、稳健性和经典性）应用于物理可实现的运算。
• 改进的有限规模界限： 该流水线被用作“发现机器”，推导出了一个更紧凑的经典-量子态条件熵方差界限。这一新不等式改进了文献 [32] 中的界限，直接降低了计算密钥长度时的有限规模惩罚项。
• 开源库： 作者发布的底层量子信息库包含了状态、通道、熵、有限规模界限以及 LOCC 语言的定义，旨在促进其他量子信息证明的复用。

结果
形式化过程得出了两个主要定理：

1. 定理 1（有限密钥安全性）： 确立了 BB84 协议的实际信道与理想信道满足可组合安全性界限 $\frac{1}{2}\|E_{real} - E_{ideal}\|_\diamond \leq \varepsilon_{QKD}$。该界限考虑了有限块大小、参数估计、隐私放大以及后选择技术（将安全性从集体攻击扩展到相干攻击）。密钥长度条件纳入了一个基于新方差界限推导出的精细化有限规模惩罚项 $P_\beta(n_K, \bar{\varepsilon})$。
2. 定理 2（稳健性）： 限制了协议在无记忆诚实信道上的中止概率，确保在不存在窃听者时，协议不会以高概率中止。

此外，定理 3 提供了改进后的条件熵方差界限：
$$V(W|B)_\rho \leq \log_2^2(\sqrt{d_W} + \sqrt{d_W - 1})$$
对于二进制密钥（$d_W=2$），这产生了一个上限 $C_\star \approx 1.6168$（比特平方），相比之前的界限 $\log_2^2 5 \approx 5.39$ 有显著提升。

意义
本文声称通过消除隐藏假设并确保证明仅依赖于 Lean 的标准公理，为量子密码学的安全性论证设定了一个可复现的标准。通过演示形式化证明引擎如何加速发现过程——具体而言是通过识别出能改善密钥率的更紧凑的熵方差界限——这项工作说明了机器检查的证明如何增强量子信息科学的可靠性和性能。作者强调，他们的库和协议语言旨在被复用于其他协议（如安全计算或多方深度学习）以及不同的安全性框架（如熵累积）。