本文研究了密码学模型认证（CMC）协议中的安全假设与实际部署之间的差距。隐私保护的机器学习审计协议允许审计员评估模型的准确性或公平性，而无需暴露模型内部或训练数据，因此特别适用于医疗、金融等敏感领域。然而，现有安全定义通常仅保证模型在固定审计数据集上的行为，未能确保这些保证推广到同一分布的其他数据集。作者展示了这一漏洞允许模型提供者通过精心设计训练数据来攻击基于零知识证明（ZKP）的CMC方案：可以生成一个在审计时表现正常（如准确率>99%），但在实际部署中表现异常（如准确率<30%）的模型。为了弥补这一差距，作者形式化了针对CMC框架的严格密码学安全概念，提出了一个通用协议模板，并证明了其满足这些要求。实验结果表明现有方法存在隐患，并为设计安全的隐私保护机器学习审计协议提供了指导。

该论文提出 CryptoBap，一个用于验证加密协议二进制代码安全属性的平台。研究背景是：现实中的加密协议实现可能因编译器优化、平台差异或编程错误而引入安全漏洞，而传统的形式化验证方法通常针对高级语言或协议规范，难以直接分析编译后的机器码。核心问题是如何在二进制层面自动验证协议的弱保密性和认证属性。方法上，CryptoBap 首先将 ARMv8 和 RISC-V 架构的协议二进制代码反编译为中间表示（IR），然后执行密码感知的符号执行，自动提取覆盖所有执行路径的协议模型。符号执行过程支持间接跳转解析和基于循环总结技术的有限循环处理，完全自动化。提取的模型通过第三方工具链转换为 ProVerif 或 CryptoVerif 可接受的输入格式，从而利用这些成熟的自动验证器完成安全属性证明。论文证明了该方法的可靠性（soundness），并通过多个案例验证了平台的有效性，包括玩具示例以及真实协议 TinySSH（SSH 实现）和 WireGuard（现代 VPN 协议）。实验结果表明，CryptoBap 能够成功提取协议模型并验证安全属性，且运行效率可接受。该工作的主要贡献在于：1）首个结合二进制翻译、密码感知符号执行和自动验证器链的集成平台；2）针对 ARMv8 和 RISC-V 指令集的支持；3）对真实世界协议的成功验证。适合的研究读者包括形式化验证、二进制分析、加密协议实现安全性领域的研究人员。

本文从表示论的角度研究密码协议中的数字表示问题。传统观点认为，只要协议中的数值是计算上可访问的即可，但本文指出，在实际协议操作中，数值的固定表示形式同样关键。论文区分了三种表示论概念：算法可逼近数（A_app，即可计算实数）、系统中有限准确可描述数（A_fin(S)）以及系统的规范可归一化性。作者证明，不存在一个可计算的扩展规范器能够将可计算实数的任意逼近程序统一转换为唯一的有限值编码。作为操作理性核心表示，论文采用有理数系统及其规范编码规范Sigma_Q（包含有效的分数描述规则、规范代码和归一化）。相应的值集为A_ex=Q。规范可序列化对象类将这一核心思想扩展到实际协议对象（如文件字节序列、哈希值、交易ID和规范性序列化载荷）。通过对称加密、非对称加密和哈希的完整示例，以及基于区块链的文件完整性验证协议snaproot哈希锚定实际案例，论文展示了数值的数学确定性和作为协议对象的操作唯一性是两个不同的需求。一旦固定了规范表示规范，字节级正确性和良定义性论证就可以在不依赖实现相关的序列化或舍入决策的情况下进行。该工作对协议互操作性、良定义性和形式化验证具有重要启示。

该论文提出了一种名为 LeanDY 的形式化验证框架，面向密码协议的安全性分析。现有工具要么全自动但表达能力有限，要么交互式证明灵活但自动化不足。LeanDY 通过结合基于类型推理（type-based reasoning）与基于轨迹推理（trace-based reasoning），实现了状态化、无界协议的模块化验证。遵循语言与自动化协同设计原则，框架为协议提供定制化自动推理，同时保持高表达力。LeanDY 作为 Lean 证明助手的库实现，扩展了 DY* 的设计，融合协议特定自动化与交互式证明。它统一支持多种功能与安全需求，包括机密性、认证以及递归条件机密性（如 XOR 协议）。论文在 LeanDY 中形式化 SegWit 风格的区块链原语，并深入验证了基于此模型支付通道的惩罚机制和链活性属性，展示了框架的表达力。该研究适合对形式化方法、密码协议验证和区块链安全感兴趣的研究者。

该论文针对形式化验证工具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实现，并预防未来因实现错误或设计缺陷引发的攻击。