AI 中文总结
本文针对QKD协议的经典控制安全性，基于ETSI和ITU-T规范构建混合模型，用Tamarin发现三类漏洞并提出测量承诺等改进，验证后已提交给标准化组织。
AI 中文摘要
量子密钥分发（QKD）协议通过量子力学原理提供信息论安全性。然而QKD本质上是混合协议，其安全性取决于量子阶段与经典后处理的正确集成。尽管ETSI和ITU-T规范对QKD架构和接口进行了标准化，但它们孤立地评估协议安全性，将跨层交互作为未充分探索的攻击面。本文引入了一种形式化验证框架，该框架基于ETSI和ITU-T QKD规范对QKD协议进行整体建模。我们的模型是首个混合QKD协议模型，支持协议级安全性的自动化分析，重点关注经典操作如何影响QKD协议量子阶段提供的安全性保证。我们在自动化协议验证工具Tamarin中，基于ETSI和ITU-T QKD规范形式化了QKD协议的综合符号模型。应用该框架，我们获得了在敌手Eve+下，基于ETSI和ITU-T的协议模型中存在三个规范级漏洞的形式化证据：被破坏的纠缠注入、基延迟测量和消息反射。每个漏洞均源于程序文本中的经典控制平面疏漏，且是在符号抽象下确立的，并非对所有实际部署的断言。我们引入了两项协议改进：测量承诺和身份绑定消息认证码（MAC）。Tamarin验证确认这些对策可消除Eve+下的已识别漏洞。我们已将结果和建议传达给相关标准化组织。
英文摘要
Quantum Key Distribution (QKD) protocols provide information-theoretic security by using quantum mechanical principles. Yet QKD is fundamentally a hybrid protocol: its security depends on the correct integration of the quantum phase with classical post-processing. While ETSI and ITUT specifications standardize QKD architectures and interfaces, they evaluate protocol security in isolation, leaving cross-layer interactions as an underexplored attack surface. This paper introduces a formal verification framework that holistically models QKD protocols based on ETSI and ITUT QKD specifications. Our model is the first hybrid QKD protocol model that supports automated analysis of protocollevel security focusing on how classical operations influence the security guarantees provided by the quantum phase of the QKD protocol. We formalize a comprehensive symbolic model of QKD protocols, based on ETSI and ITU-T QKD specifications, in Tamarin, an automated protocol verifier. Applying this framework, we obtain formal evidence of three specification-level vulnerabilities in ETSI- and ITU-T-grounded protocol models under adversary Eve+: subverted entanglement injection, basis-deferred measurement, and message reflection. Each arises from a classical control-plane omission in the procedure text and is established under a symbolic abstraction rather than as a claim about all practical deployments. We introduce two protocol improvements: measurement commitment and identitybound message authentication codes (MACs). Tamarin verification confirms that these countermeasures eliminate the identified vulnerabilities under Eve+. We have communicated our results and recommendations to relevant standardization organizations.
