该论文提出了首个面向协议计算后量子安全性的机械化证明体系。核心贡献是设计了一个新的计算一阶逻辑 PQ-BC，该逻辑相对量子攻击者是可靠的，并基于此实现了机械化证明工具 PQ-SQUIRREL（通过修改经典的 SQUIRREL 证明器并加入新策略）。PQ-BC 的构建需要对经典 BC 逻辑进行扩展，使其在单一交互式量子攻击者模型下保持可靠性，同时通过强制一组语法条件来保证工具的正确性。利用 PQ-SQUIRREL，作者完成了多个案例研究，首次给出了计算后量子安全性的机械证明，包括两个基于 KEM 的密钥交换通用构造、IKEv1 和 IKEv2 的两个子协议，以及 Signal X3DH 协议的一个后量子变体。此外，该工具还证明了许多经典的 SQUIRREL 案例研究已经具备后量子安全性。这项工作为后量子安全协议分析提供了基础性工具，填补了机械化后量子安全证明领域的空白。适合密码学协议设计者、形式化验证研究人员以及关注后量子迁移的安全工程师阅读。

远程自主代客泊车（LAVP）系统旨在缓解城市交通拥堵与停车困难，但大规模停车需求下的预约服务面临身份合法性和通信安全方面的挑战。现有方案大多聚焦于停车请求验证和入场检查，未能充分保护乘客上下车过程中的身份认证与会话安全。针对这一问题，论文提出了 SecLAVP，一种可证明安全的三因素认证与密钥协商协议。该协议结合密码、生物特征和智能卡，在上下车点（DP）的辅助下，实现乘客与自动驾驶车辆（AV）之间的双向认证，并协商建立会话密钥用于后续安全通信。安全性分析方面，作者在 Real-Or-Random（ROR）模型中形式化证明了协议具有会话密钥安全性；AVISPA 模拟验证了协议能够抵抗中间人攻击；非正式分析表明其满足 15 个既定安全目标。性能评估从通信开销、计算开销和调度三个方面展开，结果显示 SecLAVP 具备实际部署的可行性。该研究为 LAVP 预约服务提供了一套完整的安全认证框架，对车联网和智能交通系统中的身份管理与密钥协商设计具有参考价值。

本论文针对 EMV 非接触式支付系统中存在的中继攻击（relay attack）问题展开研究。中继攻击允许攻击者在持卡人与读卡器之间转发消息，从而在用户不知情的情况下完成支付，例如通过无线方式窃取资金。论文首先评估了现有的防护措施：Apple Pay 要求用户指纹或 Face ID 授权；Mastercard 和 Visa 则提出了基于时间或加密的协议来阻止中继。作者发现，在交通支付模式下，可以利用中继绕过 Apple Pay 的锁屏，从已锁定的 iPhone 向任意 EMV 读卡器非法支付任意金额，无需用户授权。此外，Visa 提出的中继对抗措施可被 root 后的智能手机绕过。对于 Mastercard 的防护，作者指出其时间限制在 ISO 14443 协议层实施比在 EMV 协议层更可靠。基于这些发现，论文提出了一种新的中继抵抗协议 L1RP（Layer 1 Relay Protection），并利用 Tamarin 证明器对手机支付（含或不含用户认证）的不同模式进行建模，形式化验证了 Apple 和 Visa 建议（Samsung 采用）的解决方案，并证明 L1RP 能够有效抵御中继攻击。该研究为改进非接触式支付安全提供了重要理论和实践依据。

现有程序验证器能够证明安全协议实现的高级属性，但由于需要大量人工努力，难以扩展到大型代码库。针对这一挑战，本文提出了一种名为Diodon的新方法。Diodon通过将代码库分割为协议实现（核心）和其余部分（应用程序）来解决扩展性问题。这种分割允许对安全关键的核心应用强大的半自动验证技术，同时通过全自动静态分析确保应用程序不能破坏为核心证明的安全属性，从而将验证扩展到整个代码库。静态分析通过证明I/O独立性来实现，即应用程序内的I/O操作与核心的安全相关数据（如密钥）无关，并且应用程序满足核心的要求。作者首先通过证明可以安全地允许应用程序执行独立于安全协议的I/O操作，其次证明手动验证和静态分析能够可靠地组合，从而证明了Diodon的正确性。评估在两个案例上进行：一个签名的Diffie-Hellman密钥交换实现，以及一个大的（10万+行代码）生产级Go代码库，该代码库实现了一个密钥交换协议。通过使用自动激活程序验证器Gobra验证约1%代码的核心，在不到3人月内获得了机密性和注记一致性保证。该方法为大型安全协议实现的可扩展验证提供了一种新途径。

本文提出Pepper，一种高带宽匿名广播协议，针对全局敌手提供加密发送者匿名性。Pepper基于双服务器DC-net架构，但引入三项关键创新：1）使用可验证分布式点函数的自包含匿名注册子协议，无需外部拨号服务；2）通过分布式多点函数支持批量消息，允许每个发送者每个epoch发送多条消息且只需单次审计；3）基于秘密共享证明的轻量级访问控制机制。与现有系统相比，Pepper显著提升了大规模数据传输的吞吐量。实现表明，Pepper达到毫秒级注册审计，可高效扩展至数千通道，有效消息速率比最先进方案高1.2至20倍。此外，Pepper设计注重实际部署，能与Tor和联邦社交网络自然兼容。该研究主要贡献在于突破了DC-net在带宽和可扩展性上的瓶颈，并提供了实用的匿名广播方案。