本文针对一个此前缺乏系统认识的问题展开研究：大语言模型（LLM）在密码协议的符号化验证（symbolic protocol verification）中究竟能起到多大作用。作者指出，LLM 已在软件工程与安全分析任务中表现出较强潜力，但其在密码协议形式化验证这一高度专业化、对正确性要求极严的领域中的实际能力尚不明确，因此开展了（据作者所述）首次系统性评估。 核心方法上，论文提出了一种基于证明的度量指标 CRoST（Coverage Rate of Solve Tree，求解树覆盖率）。该指标从验证器生成的证明骨架（proof skeleton）出发，衡量 LLM 自动生成的引理（lemma）与人工参考引理之间的相似程度，从而把“LLM 辅助验证的效果”量化为可比较的覆盖率数值。作者通过理论分析与实证验证两条路径论证了 CRoST 这一指标的合理性，使其不只是经验性的打分，而具备一定的解释依据。 实验结果显示：当前最先进的模型在协议验证任务上平均仅达到 38.82% 的覆盖率，但其中有 14.4% 的生成引理覆盖率超过 80%，说明 LLM 已经能够在一定程度上产出对验证真正有用的引理，并非完全无效。与此同时，论文揭示了三类明显的失败模式：一是面对复杂的多阶段协议时表现不佳；二是在朴素地扩大模型规模或采样规模时收益递减，暗示单纯 scaling 难以解决问题；三是产生可观的验证开销，即 LLM 生成的候选引理需要形式化验证器反复求解，代价高昂。 论文的贡献可归纳为：给出首个系统性的 LLM 协议验证能力评估、提出并验证 CRoST 度量、量化当前能力上限与失败模式，并据此为面向真实复杂协议的后续研究指明方向（如更好的引理筛选、搜索策略与开销控制）。该工作适合形式化方法与协议安全研究者、以及尝试把 LLM 引入验证工具链的工程团队阅读。

该论文研究混合密钥建立（hybrid key establishment）在缺少握手上下文认证时的降级风险。混合方案同时运行一个后量子 KEM（当前标准化的 ML-KEM）与一个经典 Diffie-Hellman 原语，使得只要其中任一组件未被攻破，会话密钥即保持安全；这一设计已被 TLS、SSH 和 IKE 标准化采纳。作者指出一个被普遍忽视的缺口：混合 KEM 只保护派生密钥的机密性，却不保护"选用哪些原语"这一协商过程本身的完整性。完整协议依靠握手 transcript 对协商结果做认证，但当混合 KEM 作为独立 drop-in 原语部署，或置于不做 transcript 认证的精简握手中时，这种保证便不复存在，主动攻击者可以剥离后量子选项实现降级。论文提出的核心问题是：密钥调度（key schedule）自身必须包含什么内容，才能使抗降级成为 combiner 的局部属性，而不依赖外层协议。方法上，作者在 combiner 层给出基于游戏（game-based）的形式化安全定义，并证明了一个双向分离（two-sided separation）结论：忽略 transcript 的 combiner 必然可被降级；而把会话密钥与确认标签（confirmation tag）都绑定到 transcript 哈希的 combiner 则能阻止所有此类尝试，其残余优势项对 256 位 transcript 哈希而言可忽略。论文还给出显式的"最强链路"（strongest-link）安全界，刻画混合组合的安全强度。成本方面，作者基于已公开发表的 Cortex-M4 测量数据构建标定成本模型，结果表明 transcript 绑定每方仅增加一次哈希运算，约占握手计算量的 11.8%，但仅占包含无线电通信在内的总能耗的 1.5%，且不增加任何报文数量或线上字节开销。所有报告数值均由已发布的测试框架（harness）生成，并通过 30 项校验门。该工作适合密码协议设计者、PQC 迁移与 TLS/SSH/IKE 实现者，以及嵌入式安全工程师阅读。

该论文针对密码学协议形式化验证工具的实际使用体验开展了一项以人为中心的探索性研究。作者指出，Tamarin、ProVerif 等协议验证工具已被广泛用于分析复杂协议的安全性，但用户如何与这些工具交互、在哪里受阻，长期以来缺乏系统性研究。为此，研究团队面向具备实操经验的用户群体（包括科研人员、研究生与工业界实践者）开展问卷调查，覆盖 Tamarin、ProVerif 及相关协议验证器的使用者。研究结果显示，可用性障碍贯穿整个验证工作流：首先是调试困难，尤其是证明过程不终止（non-termination）与性能退化问题时，用户难以定位原因；其次是缺乏系统化方法，用于验证形式化模型是否忠实反映真实协议，即模型与现实协议之间可能存在的语义偏差难以被发现。在证明失败且未给出具体攻击路径的情况下，用户普遍采取三类应对策略：简化模型、添加辅助引理（helper lemmas）、回溯并重新审视建模抽象层次。参与者还明确提出了若干改进诉求，包括可操作的诊断信息、对验证结果更清晰的解释、可视化支持，以及针对重复性证明任务的自动化能力。作者进一步归纳出一个核心洞察：持续的可用性挑战源自“协议层推理”与“验证器的形式化模型、证明过程、诊断输出”之间的鸿沟，即用户以协议语义思考，而工具以形式化演算和求解器状态回应。基于这些发现，论文提出了面向设计者的具体优先级，旨在提升密码学协议验证工具的可访问性、可解释性与易用性。该工作属于人机交互与形式化方法交叉方向的实证研究，适合协议设计者、形式化验证工具开发者、以及将验证工具引入安全工程流程的团队阅读。

论文《Efficient and Secure Range Counting over Distributed Geographic Data with Query Range Protection》解决了分布式地理数据中范围计数查询的隐私保护问题。现有方案要么泄露查询范围，要么因使用昂贵的安全比较操作导致效率低下，且大多假设数据不重叠，导致重叠场景下误差巨大。本文提出PPRC协议，同时满足隐私、效率和准确性要求。主要技术贡献包括：1）私有范围谓词（PRP）技术，将范围评估转化为加密成员测试，用高效的安全乘法替代昂贵的比较操作，从而保护查询范围；2）遗忘线性计数（OLC）聚合方案，仅使用轻量级密码操作安全聚合重叠数据组织的部分结果，不泄露最终计数以外的任何信息。理论分析和实验表明，PPRC相比基线协议误差最多减少55倍，速度提升最多37倍。该工作适用于多机构间的地理数据联合分析场景，如灾害响应、人口统计等，为实际部署提供了可行性。

该论文针对大规模语言模型（LLM）对话记录在数字取证和合规审计中日益重要的应用背景，指出传统的线性防篡改日志无法捕捉LLM对话内在的非线性演化特性，例如基于历史查询的重新提示、回复重生成、会话删除、多设备并发以及选择性分享。为解决这一问题，论文提出了一种可验证的对话记录系统（Verifiable Conversation Transcript, VCT），将复杂的非线性LLM语义操作抽象为账户级别的认证状态转换。VCT构建了一个三层密码学数据结构：原子问答对形成分支级哈希链，分支尾部聚合为会话级Merkle根，所有会话根进一步聚合并由用户和服务器的联合签名锚定为账户级Merkle根。VCT引入了一种带有删除屏障的序列化状态转换协议，以消除删除与修改之间的冲突，并辅以确定性状态合并协议，以保留并发的非删除增量操作。此外，增量否认检查和八卦协议使异步用户设备能够自主检测恶意服务器导致的视图分叉，并生成不可抵赖的取证证据。安全分析表明，在标准密码学假设下，VCT保证了账户级对话记录的完整性、一致性、可验证共享性和不可否认性。在Python原型上的评估显示，核心操作的密码学延迟在亚毫秒到低毫秒范围内；在21KB文本的实际配置下，安全元数据仅引入0.9%的存储开销，验证了VCT在高风险取证审查场景下部署于生产级LLM平台的可行性。