本文对互联网工程任务组（IETF）发布的征求意见书（RFC）中的安全考量章节进行了首次大规模实证研究。RFC 是互联网核心协议的标准、备忘录及相关技术文档，自20世纪90年代初起，每篇 RFC 被要求包含专门的安全考量章节。作者从多个维度分析了这些章节的内容与演化。研究发现：（1）超过90%的抽样 RFC 在安全章节中明确讨论了安全问题；（2）尽管安全考量是强制要求，但其中极少（甚至从未）施加强制性的安全需求；（3）以安全考量章节为基础的 RFC 引用网络整体较为稀疏，但少数核心 RFC 及其安全章节被大量引用；（4）引用量在1990年代中期至2010年代中期达到峰值；（5）这些章节所讨论的主题并不代表常见的一般性安全问题（如欺骗、窃听等），而大多反映的是各协议特有的安全问题；（6）除通用网络安全、安全规范和路由外，主题的纵向演化也呈现出协议特异性。此前尚无针对此课题的系统研究，因此本文填补了标准化文献中的空白。研究方法和发现对理解互联网标准中的安全实践演进具有重要参考价值，适合标准化研究者、协议设计者和安全政策制定者阅读。

量子密钥分发（QKD）协议通过量子力学原理提供信息论安全性，但实际部署中QKD本质上是混合协议：其安全结论高度依赖量子阶段与经典后处理阶段的正确集成。虽然ETSI和ITU-T等标准组织已定义了QKD的架构与接口，但现有规范通常在隔离条件下评估协议安全性，导致跨层交互成为未被充分探索的攻击面。本文提出一种基于ETSI和ITU-T QKD规范的形式化验证框架，首次在混合协议模型下对QKD进行自动化协议级安全分析，重点考察经典操作如何影响量子阶段所提供的安全保证。作者使用自动化协议验证工具Tamarin，构建了符合ETSI/ITU-T规范的QKD协议综合符号模型。在该框架下，作者针对名为Eve+的敌手模型，获得了三项规范级漏洞的形式化证据：被颠覆的纠缠注入（subverted entanglement injection）、基延迟测量（basis-deferred measurement）和消息反射（message reflection）。这些漏洞均源于规范程序文本中经典控制平面的某种缺失，且仅在符号抽象下成立，并非对所有实际部署的普遍断言。为缓解这些问题，作者提出两项协议改进：测量承诺（measurement commitment）和身份绑定消息认证码（identity-bound MACs）。Tamarin验证表明，这些对策能够消除Eve+模型下识别出的漏洞。研究结果和建议已发送给相关标准化组织。本文的贡献在于首次以形式化方法系统性地将经典控制面纳入QKD协议安全分析，揭示了标准规范中被忽略的跨层风险，为QKD协议的设计与标准化提供了可验证的改进方向。适合QKD协议设计者、密码学标准化人员以及形式化方法安全研究者阅读。