本文对IETF QUIC协议记录层的安全性进行了系统研究。QUIC是传输层协议，其记录层负责数据包加密和头部保护，IETF标准第30版相比Google原始协议和早期草案有重大变化。作者首先提出了一种新的安全定义——带半隐式nonce的认证加密（AE with semi-implicit nonces），以精确刻画QUIC的隐私保护目标。他们证明QUIC使用的加密构造是通用构造的一个实例，该通用构造以标准AEAD安全方案和PRF安全密码为参数。通过形式化验证工具F*，作者对该构造进行了安全证明，并发现了短头部可塑性以及数据包计数器最低有效位数选择导致nonce机密性受限于特定弱点，进而提出了增强鲁棒性的改进方案。除安全模型外，作者还给出了记录层的具体功能规范，修复了草案中的多处错误后，证明了正确解密等关键功能的正确性。最后，他们实现了经验证内存安全、符合规范且具备安全属性的高性能记录层，吞吐量接近2 GB/s。面向防御者的价值在于：该工作为QUIC记录层的安全性提供了严格的形式化基础，揭示潜在设计局限并提出改进，有助于构建更安全的QUIC实现，并预防未来因实现错误或设计缺陷引发的攻击。

本文（系列第6篇）聚焦后量子密码学中基于NTT（数论变换）硬件的算术掩码组合安全性。布尔掩码的组合理论（NI、SNI、PINI）已成熟，但素数域上的算术掩码（NTT后量子密码的基础）缺乏类似理论。作者提出并形式化证明了素数域上PINI（Prime-Field PINI）的组合定理。核心见解是“更新参数”（renewal argument）：当在两个流水线阶段间施加新的随机掩码时，中间导线无论第一阶段的防护参数如何都会变得完全均匀。对于两个PF-PINI gadgets（参数k1和k2），经新鲜掩码组合的两阶段流水线满足PF-PINI(k2)，阶段1的多重性被完全消除。无新鲜掩码时，中间导线多重性可达k1，构成差分功耗分析的必要条件。作者在Lean 4中形式化了两个定理，包含18个机器检查的证明，零个“sorry”存根。他们还形式化地桥接了Barrett约简的代数模型与硬件忠实算术模型，并实例化定理以正式诊断微软Adams Bridge PQC加速器：其缺失阶段间新鲜掩码导致Barrett输出导线在一阶探针模型下非均匀，这一架构缺陷与三个独立实证分析一致。计算证据进一步表明“1比特屏障”在Barrett和Montgomery约简中具有普遍性。本文适合对后量子密码侧信道防护、形式化验证与硬件安全感兴趣的研究者阅读。