本研究对 Signal 协议的核心组件——双棘轮（Double Ratchet）机制进行了自动形式化安全分析。双棘轮负责在消息丢失、重排序或临时密钥泄露等复杂条件下提供前向安全和后向安全。研究者使用 ProVerif 工具（一种自动密码协议验证器）对双棘轮协议建立精细模型，并首次发现了在特定场景下可导致密钥安全属性失效的攻击：当一条消息在发送者密钥状态被更新后丢失，且攻击者恰好获取了该丢失消息之前的状态信息时，可能恢复后续会话密钥的部分信息。这一攻击突破了双棘轮设计者声称的安全保证。随后作者提出了两种修复方案：一是修改密钥派生结构，增加额外的哈希迭代；二是调整连锁密钥的更新规则。通过 ProVerif 自动验证，修复后的协议满足预期的安全属性。论文还对修复方案给出了严格的安全性证明，并讨论了形式化分析在现实密码协议设计中的重要性。该工作为即时通讯软件的安全加固提供了理论依据，也展示了自动形式化验证工具在发现真实协议漏洞方面的有效性。

该论文针对智能交通系统中车辆与基础设施间安全通信的关键需求，聚焦于恶意或异常车辆密码凭证的及时撤销问题。当前标准对撤销处理规定模糊，现有方案在可扩展性和有效性方面存在严重局限。为此，作者提出了一种形式化验证的车辆自撤销机制，该机制利用车辆中的可信处理元素（TPE），但不依赖可信时间源，从而避免了时间同步的脆弱性。方案兼容现有标准化工作，并首次利用Tamarin证明器保证撤销的确定性和可预测的上界，即使在存在现实攻击者（如网络延迟、消息丢失）的情况下也能确保撤销的实效性。作者在虚拟5G-Edge部署场景中模拟了大量车辆通信的真实环境，包括网络故障和延迟，实验结果表明该机制在保持形式化保证的同时，具有低网络开销和良好的可扩展性。该工作对V2X安全基础设施的改进具有重要参考价值。

5G核心网作为下一代移动通信网络的核心，其访问控制机制的安全性至关重要。然而，由于5G核心网的复杂性，传统的安全分析手段难以全面覆盖其访问控制策略的潜在缺陷。本文提出5GCVerif，一个基于模型测试的形式化分析框架，专门用于分析5G核心网的访问控制机制。5GCVerif采用模块化设计，通过多种抽象技术构建能够捕捉5G核心网访问控制机制复杂细节的抽象模型，从而解决了模型检查中的状态爆炸问题。此外，5GCVerif通过将模型检查器的探索范围限制在有效的网络配置内，避免了为所有可能的核心网配置生成模型的难题。利用5GCVerif，作者评估了55个安全属性，发现了5个新的访问控制漏洞。这些漏洞可能导致未授权访问敏感信息、非法访问服务以及拒绝服务等多种攻击。该研究表明，形式化方法在发现5G核心网安全漏洞方面具有显著效果，为5G网络的安全设计和验证提供了有力工具。

该论文聚焦于分布式信息物理系统（如物联网、自动驾驶汽车）的安全建模与验证问题。传统建模方法在面对动态成员和复杂交互时变得笨重且不实用，例如多车交互场景中车辆相对位置和车道变化带来的挑战。为此，作者提出了一种以自我为中心的抽象方法，用于简洁地建模任意数量代理围绕一个自我代理的局部交互。这种模型抽象掉其他代理的详细行为，并忽略存在但物理上远离的代理。论文展示了该方法能够捕捉自动驾驶汽车责任敏感安全（RSS）框架中的有趣场景。作为分析示例，作者利用以自我为中心的模型证明了多个高速公路驾驶场景的安全性，证明过程中凸显了经典验证方法——归纳不变断言的力量。最后讨论了该分析方法向其他场景和应用的推广可能性。论文主要贡献在于提出了一种新颖的建模抽象，降低了分布式系统安全验证的复杂性，并通过自动驾驶案例验证了其有效性。适合研究形式化方法、系统安全验证以及自动驾驶安全的研究人员和工程师阅读。

本文针对密码系统侧信道攻击的掩码防御机制，提出了一种基于概率分离逻辑的形式化验证方法，用于自动验证掩码算法的非干扰性安全属性。作者首先建立了非干扰性与条件独立性之间的数学联系，从而将安全验证问题转化为条件独立性推理问题。随后，利用现有的Lilac分离逻辑框架（该框架专用于条件独立性推理）来执行验证，并设计了一系列新的证明规则，以支持探测安全性的高效验证。通过若干示例算法，论文展示了该方法能够有效验证典型掩码方案的安全性，同时相比传统手工证明或模型检验方法，降低了误判风险。该工作主要面向密码学实现者、安全验证工具开发者以及侧信道防御研究者，其核心贡献在于为掩码算法的形式化安全验证提供了更简洁、可自动化的理论框架。

论文提出了一种混合形式化验证方法，结合高层演绎推理和电路级推理，用于高度优化的加密汇编代码。该方法在 EasyCrypt 证明助手中扩展实现，通过使用等价性检查将安全保障传播到同一计算的不同优化或不同架构的实现中，从而降低低级别函数的证明工作量，并分摊证明开销。论文以 ML-KEM（一种后量子密码算法）在 Jasmin 中的形式化验证实现为例，首次获得了在 x86-64 架构上性能与最快非验证实现相当的形式化验证实现。这证明了混合方法在兼顾性能与安全性方面的有效性。研究背景在于现有形式化验证方法在处理深度优化汇编代码时面临可扩展性挑战，而本文结合两种推理范式，利用电路级推理处理底层优化细节，利用演绎推理处理高层语义，显著提升了验证效率。实验结果表明，该方法能够在保持高性能的同时实现形式化安全保障，适合对密码学实现安全性和正确性有高要求的场景。

本论文针对后量子密码（PQC）硬件实现中的掩码Barrett reduction的侧信道泄漏问题，提出首个通用且机器验证的基数界限——1-Bit Barrier。Barrett reduction是基于NTT的PQC实现（如ML-KEM、ML-DSA）的非线性核心，但现有组合框架（ISW、t-SNI、PINI、DOM）仅针对GF(2)上的布尔掩码，无法直接应用于素域上的算术掩码。作者基于此前系列工作（QANARY、partial-NTT-masking margins、代数基础、蝴蝶组合），填补了这一空白。核心贡献在于：1）证明对于任意模数q>0和移位s，Barrett内部导线映射f_x(m) = ((x + 2^s - m) mod 2^s) mod q的原像基数属于{0,1,2}，绝不超过2——这一性质被称为1-Bit Barrier，意味着每条内部导线最多泄露1比特的最小熵；实际泄漏通常更少，因为计数为0的情况（不可达输出值）使界更为保守。2）引入PF-PINI（素域PINI）概念，证明Barrett满足PF-PINI(2)，Cooley-Tukey蝶形运算满足PF-PINI(1)，并观察到在阶段间加入新鲜掩码时，组合管线的最大原像基数为max(k1, k2)，因此1-Bit Barrier可传播。3）在Lean 4（Mathlib）中完成了12条定理的机器验证，无一个“sorry”，结果对所有q>0通用。4）指出Adams Bridge因缺少阶段间新鲜掩码而违反PF-PINI组合，解释了此前发现漏洞的原因。该工作为NIST IR 8547推荐的形式化方法在PQC实现验证中提供了首个通用机器验证的基数界，并给出1比特泄漏的直观解释。适合侧信道分析、PQC硬件安全、形式化验证领域的研究者和工程师阅读。