本文针对函数秘密共享（FSS）中存在的密钥生成依赖可信第三方这一安全瓶颈，提出了高效的分布式密钥生成方案。FSS作为一种重要的安全计算工具，其在线阶段交互轮次恒定且效率极高，但传统方案中密钥生成需由可信第三方集中完成，这既带来了单点安全风险，也限制了实际部署的灵活性。作者首先为基于FSS的分布式点函数和分布式比较函数设计了分布式密钥生成协议，支持输入和输出均为算术共享形式，从而消除了对任意可信实体的依赖。在此基础上，论文进一步构建了若干关键FSS基础组件，这些组件针对在线效率进行了深度优化，可作为高级协议的可复用构建模块。最后，文章提出了一种高效框架，用于评估科学计算中普遍存在的复杂三角函数。该框架巧妙利用三角函数的周期性，在FSS评估过程中有效缩减输入的比特长度，从而缓解了比特长度增长对FSS协议性能的潜在瓶颈。通过大量针对真实应用场景的实验评估，结果表明，与当前最优工作相比，本文方案在延迟上最高降低14.73倍，通信开销减少27.67倍至184.42倍。该研究适用于对安全计算、密码学协议及数据隐私保护感兴趣的研究人员和工程人员。

该论文对Matrix协议的核心组件——设备导向的群组消息系统——进行了正式密码学分析。Matrix是一种去中心化的实时通信协议，广泛应用于安全即时通讯场景。作者通过建立精确的安全模型，定义了设备导向群组消息的密码学目标（如端到端加密、前向安全性、后向安全性和组内一致性），并证明了Matrix当前设计在某些假设下能够满足这些安全属性。分析揭示了协议中可能存在的细微安全假设依赖，并提出了改进建议。该研究为理解Matrix协议的安全性提供了严格的理论基础，并有助于指导未来群组通信协议的设计与验证。

本文是系列论文的第6篇，专注于后量子密码中基于数论变换（NTT）的掩码硬件的形式化验证。此前，布尔掩码的组成理论（如NI、SNI、PINI）已成熟，但素数域Z_q上的算术掩码（NTT后量子密码的基础）缺乏类似理论。本文首次提出了素数域上算术掩码的机器检查组合定理。核心洞察是“更新论证”（renewal argument）：在两个流水线阶段之间施加一个新鲜随机掩码时，中间线变得完全均匀，与第一阶段的安全参数无关。具体地，对于两个PF-PINI gadget（参数为k1和k2），如果组合时使用新鲜掩码，则两级流水线满足PF-PINI(k2)，第一阶段的多重性被完全消除；若没有新鲜掩码，中间线的多重性可达k1，为差分功率分析（DPA）创造必要条件。作者在Lean 4中形式化了两个定理，包含18个机器检查的证明，无任何“sorry”存根。他们还正式建立了Barrett约简的代数模型与硬件忠实模型之间的桥梁，并将定理实例化，用于诊断微软的Adams Bridge PQC加速器：缺乏级间新鲜掩码导致Barrett输出线在一阶探测模型下非均匀，这与两个独立的实证分析[3,4]及他们先前的结构分析[1]发现的架构缺陷一致。计算证据进一步表明，“1位屏障”（1-Bit Barrier）在Barrett和Montgomery约简中是普遍存在的。该工作为后量子密码掩码的形式化验证提供了关键理论基础，直接揭示了实际PQC硬件中的设计漏洞。

本文研究信息论安全的分布式点函数（ITDPF）的密钥长度优化问题。分布式点函数允许将点函数 f_{alpha,beta}(x) 拆分为 n 个份额（密钥），分发给 n 个服务器，每个服务器可用其密钥计算 f_{alpha,beta}(x) 的加法份额，同时任意不超过 t 个服务器无法获取函数任何信息。现有完全安全的 1-private ITDPF 存在密钥长度较长的不足。本文基于 Ghasemi、Kopparty 和 Sudan 在 STOC 2025 上提出的私有信息检索（PIR）方案，设计了一种新的份额转换方法，构造了一个完全安全的 1-private ITDPF，输出群为 Z_p（p 为任意素数）。与现有同输出群的完全安全 ITDPF 相比，新方案的密钥长度在渐近意义上更短，效率更高。该成果对安全多方计算、秘密共享、隐私保护等底层密码原语的性能提升具有理论价值。

本文提出无条件安全的信息论认证PIR（itAPIR）构造，形式化定义其安全性，证明itPIR-RV可零开销升级为itAPIR，填补了理论空白。