该论文提出了一种在量子随机预言机模型（QROM）下实现无条件安全认证随机性的协议。该协议是非交互式的，且可由经典验证者公开验证，其设计基于 Yamakawa 和 Zhandry 在 JACM'24 上提出的量子性证明（proof of quantumness）技术。与以往依赖额外结构（如 Aaronson-Ambainis 猜想）或仅能抵御低查询深度攻击者的方案不同，本协议的安全性证明针对的是能够对随机预言机进行亚指数次自适应量子查询的 adversaries，且不依赖任何未经证明的猜想，实现了‘无条件安全’（即安全性仅基于量子力学基本定律和随机预言机模型的形式化假设）。论文的核心贡献在于：第一，首次在仅有经典验证者且协议为单轮的情况下，实现了对强量子攻击者的可证明安全随机性生成；第二，消除了此前工作中需要的结构化假设或对查询深度的限制；第三，为量子计算优势的验证提供了新的理论工具。该工作属于量子密码学与计算复杂性理论的前沿研究，适用于量子安全协议设计、随机性生成基础设施以及量子计算能力认证等研究方向。

本文研究近似同态加密（approximate homomorphic encryption）中噪声泛洪（noise flooding）防御手段在自适应解密攻击下的安全性证明问题。噪声泛洪是抵御解密攻击的标准技术，但其安全证明对组合方式异常敏感：若用统计接近的模拟替换 q 次自适应解密应答，并采用普通混合论证，则会损失线性因子 q。传统密码学证明改为累积条件 KL（Kullback-Leibler）散度成本，并在最后一次性转换为统计距离，从而获得参数关键的平方根损失。作者使用 Rocq 证明助手和 SSProve 框架对该论证进行机器验证。针对任意满足近似正确性和 IND-CPA 安全的全同态加密方案，他们形式化了对于任意 q 次查询的 IND-CPAD 攻击者的归约，并证明了攻击优势上界为 β_CPA(B_A,q) + sqrt(qn)/(2γ)，其中 n 是明文维度，γ 是泛洪宽度乘子。证明过程中构建了一种基于 SSProve 语义的新型关系程序逻辑，其毕达哥拉斯判断（Pythagorean judgment）能够组合条件 KL 预算而无需转换为统计距离；同时，一个经过验证的迹编译器将局部预言机规则提升到任意自适应程序，且仅需一次最终转换。该工作的核心贡献在于：为自适应场景下噪声泛洪安全性提供了机器可验证的证明框架，解决了混合论证中线性损失与平方根损失之间的微妙权衡问题，并为同态加密安全性证明的机械化奠定了基础。适合对密码学形式化验证、同态加密安全性分析以及程序逻辑感兴趣的科研人员与安全工程师阅读。

本文提出了一种基于图论的自动化验证框架 GAuV，用于验证多方计算（MPC）协议在完美半诚实安全模型下的安全性。传统上，MPC 协议的安全性证明依赖于针对具体协议手工构造模拟器，并对其输出分布与真实世界损坏方视图进行理论分析，这一过程繁琐且容易出错。此外，即使协议在理论上是安全的，实现过程中的粗心也可能引入安全漏洞，且难以检测。GAuV 框架能够自动验证 MPC 协议实例的完美安全性，具有完全的可靠性（soundness）：任何通过该框架验证的协议，在模拟器定义的语义下也是安全的。作者还证明了框架的完备性，即对于任何 BGW 协议实例，该框架都能在多项式时间内验证其对于所有损坏方集合的安全性。与以往仅关注黑盒隐私（即损坏方输出不泄露诚实方输入信息）的工作不同，GAuV 有潜力用于验证任意 MPC 协议的安全性。作者实现了原型系统，评估显示原型能在合理时间内自动证明 BGW 协议和 B2A（二进制到算术）转换协议的完美半诚实安全性。该研究为 MPC 协议的安全性验证提供了自动化工具，有助于减少手工证明的复杂性和实现错误带来的风险。

本论文研究了大规模群组通信中的密钥协商协议，重点关注MLS（Messaging Layer Security）工作组提出的TreeKEM协议及其变体。TreeKEM是当前IETF MLS草案中采用的连续群组密钥协商方案，但其动态操作（如增减用户）存在效率问题。论文形式化并分析了一种名为Tainted TreeKEM（TTKEM）的变体，该变体最初由Millican在MLS邮件列表中提出。TTKEM通过让新加入的节点继承其父节点的部分密钥材料（即“tainted”），从而在某些群组操作分布下比TreeKEM更高效，论文通过模拟量化了这种效率提升。此外，论文给出了TTKEM的两项安全性证明，分别针对随机预言机模型和标准模型，实现了后向安全和前向安全，并能抵抗自适应攻击者（即攻击者可以自适应地选择操作序列）。在此之前，没有任何针对类TreeKEM协议在自适应攻击者下建立紧致安全性证明的工作。论文还首次证明（甚至形式化）了主动安全（active security）场景，即服务器可以任意偏离协议规范的情况。不过，完全主动安全（用户也可任意偏离）仍未解决。本工作适合密码学研究者、安全协议设计者以及MLS标准制定者阅读。