该论文针对形式化验证工具ProVerif和Tamarin在安全协议验证中的使用门槛问题，提出了一种系统化的、基于证据的安全属性分类法。通过系统综述2022-2025年间使用这两种工具的53篇近期研究，论文提取并整理了当前被实际验证的安全属性集合，将其分为多个类别并给出非形式化的直观定义，同时用一阶逻辑给出了严格的形式化定义以确保清晰性和一致性。此外，论文还提供了在ProVerif和Tamarin中建模这些属性的通用模式，并在开放仓库中收录了可执行的示例代码，从而弥合了理论安全属性定义与实际可执行验证模型之间的鸿沟。该工作有助于安全协议设计者（而非形式化验证专家）更便捷地使用形式化工具来表达和验证协议的安全需求，对推动形式化验证在安全社区的普及具有重要意义。

本文提出FLUTE协议，用于安全多方计算（MPC）中快速且安全的查找表（LUT）评估。传统的布尔电路在安全计算中存在较大的在线阶段开销，而查找表可以替代传统门电路（如AND、XOR），生成更紧凑的电路，并显著提升在线性能。已有工作利用LUT实现了安全浮点计算和隐私保护机器学习推理，但存在设置阶段开销大或在线性能不足的问题。FLUTE在两方设定下，通过创新的协议设计，在保持与最佳先前LUT协议相当的整体性能的同时，在线阶段性能提升达两个数量级。核心方法包括优化预处理阶段和在线阶段的通信轮次与计算量。作者还提供了基于Rust语言的开源实现，以及ABY2.0和silent OT布尔安全两方计算协议的实现。实验结果表明，FLUTE在在线阶段的延迟和通信量上均显著优于现有方案，为安全计算的实际应用提供了更高效的LUT评估工具。

该论文提出了一种新型环签名方案——Deanonymizable Scoped Linkable Ring Signatures (DSLRS)，旨在同时实现作用域可链接性与去中心化问责。传统的环签名虽能提供匿名性和签名者自主组成的灵活性，但在需要链接性和问责性的场景（如医疗保健中的同意管理）中有所欠缺。现有方案要么无法在单一签名中原生集成作用域可链接性和去中心化问责，要么依赖单独的承诺或中心化开放者。DSLRS 的核心创新包括：(1) 使用作用域（上下文标识符）和动态密钥镜像，实现在同一作用域内签名可链接、跨不同作用域不可链接；(2) 在签名中嵌入两个 ElGamal 组件，并利用一个由 k-of-N 节点组成的去中心化去匿名网络，协作提取签名者的公钥，从而实现去中心化问责。该方案在随机预言机模型下基于椭圆曲线离散对数问题 (ECDLP) 和决策性 Diffie-Hellman (DDH) 假设被证明安全，并给出了正式的安全定义和约简证明。最后，论文展示了一个基于区块链的同意管理应用实例，使用 DSLRS 来管理患者对医疗数据的授权。该研究为需要匿名性与问责性平衡的隐私保护应用提供了新的密码学原语。

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