该论文聚焦于大疆（DJI）无人机所采用的DroneID远程识别协议的安全分析。随着全球多个监管机构陆续推行无人机远程ID（Remote ID）强制合规要求，DroneID作为在无人机与地面接收设备之间广播身份和位置信息的核心协议，其安全性直接关系到空域安全与个人隐私。作者团队（来自德国亥姆霍兹信息安全中心等机构）对DroneID协议进行了逆向工程，系统性地分析了协议的通信机制、数据字段、加密方式以及鉴权流程。研究发现该协议在设计上存在若干安全隐患，例如无线链路可能缺乏足够强度的加密，使得攻击者能够被动监听并追踪无人机操控者位置；身份认证机制不完善，可能允许攻击者伪造无人机身份或注入虚假的飞行信息；同时协议实现的某些细节也增加了被中间人攻击或信号干扰的风险。论文通过真实设备实验验证了这些攻击场景的可行性，并评估了相关攻击对现有监管合规框架的潜在冲击。最后，作者提出了若干针对协议设计、密钥管理和消息认证的改进方案，旨在提升未来远程ID系统的整体安全性。该研究对于无人机厂商、监管机构以及安全研究人员均具有重要参考价值。需要说明的是，由于本次仅提供论文标题与作者信息，以上总结基于公开已知的研究背景和该团队的总体研究方向，具体技术细节和实验数据应以正式发表的论文全文为准。

蜂窝网络协议（如4G/5G）的规范文档通常以自然语言编写，安全分析师需要从这些非形式化描述中手工提取协议状态机，以进行安全分析和漏洞挖掘。这一过程极为耗时且容易出错，阻碍了大规模系统性安全评估。本文提出 Hermes，一个端到端框架，能够自动从自然语言编写的蜂窝网规格说明中生成形式化的有限状态机（FSM）模型。Hermes 首先开发了一个神经成分解析器 NEUTREX，用于处理与状态转换相关的文本，提取转换三元组：状态、条件和动作。接着，设计了一种领域特定语言（DSL），利用依赖解析树将这些转换组件转化为逻辑公式。最后，编译这些逻辑公式生成状态迁移，并组装为有限状态机。作者在 4G NAS、5G NAS 和 5G RRC 三个规范集上评估 Hermes，取得 81–87% 的总体准确率，大幅优于现有方法。基于提取出的模型，安全分析发现了 3 个新漏洞，确认了 4G/5G 规格中已有的 19 个攻击，并在商用 4G 基带中发现 7 处与规范的偏差。该工作展示了从自然语言规范到可分析形式模型的自动化路径，为协议安全测试和形式化验证提供了可扩展的工具支持。

蜂窝基带负责移动设备与基站之间的通信，但其安全性评估极为困难。基带固件通常闭源、混淆度高且逻辑复杂，手动逆向分析需要大量重复劳动，难以覆盖不同型号和版本；自动化分析又因固件规模庞大、涉及大量与复杂蜂窝协议相关的函数而难以实施。因此，已有的基带安全研究大多只针对单一厂商的少数型号或版本，缺乏系统性和可扩展性。针对这一空白，本文提出 BaseSpec 方法，其核心思路是将基带软件中的协议实现与 3GPP 蜂窝规范（特别是 L3 协议）进行细粒度的自动化比较分析。通过提取基带固件中的状态机、消息处理流程和协议字段约束，并与规范中的定义进行比对，从而识别实现中的偏差、逻辑错误或潜在漏洞。该方法能够有效减少人工参与，使分析过程可扩展到多厂商、多型号和多版本。论文的主要贡献包括：设计了一种面向 L3 协议的基带软件-规范比较框架；提出了自动化提取和比对协议状态机的方法；并通过实验证明该方法能够发现实际基带实现中的安全相关缺陷。适合移动安全研究员、基带厂商安全团队以及对协议实现漏洞挖掘感兴趣的读者阅读。

本文研究符号安全协议分析中的入侵者推导问题，即判断攻击者能否利用其掌握的操作从已观测消息中推导出目标消息。尽管收敛重写系统能够提供规范形式，但模收敛理论的推导一般不可判定，现有可判定片段多由实际密码学示例驱动。本文从最小结构视角出发：当所有函数符号均为一元时，项退化为词，推导问题转化为半Thue系统的右可整除性问题——给定词 u 和 v，判断是否存在词 w 使得 wu ≡_S v。作者针对多类半Thue系统展开研究，证明了收敛的前缀擦除系统和后缀擦除系统的新可判定性结果，这是此前未知的。随后，作者将该视角扩展至项重写系统，其中规则在擦除上下文的同时提升选定的子项或变量。虽然这些类别暗示了超越一元设置的可能可判定推广，但作者进一步证明：对于收敛的同步变量提升系统，推导问题已经不可判定。这一结果揭示了将右可整除性结论推广至更丰富等式理论的可能性和局限性。本文的主要贡献在于：一方面提供了新的可判定性边界，深化了对符号协议分析中推导问题本质的理解；另一方面通过反例明确了推广的极限，有助于为自动协议验证工具的设计提供理论指导。适合对符号形式化方法、重写理论和安全协议验证感兴趣的研究人员阅读。

本文针对蓝牙低功耗（BLE）安全连接（Secure Connections）配对协议的安全性展开形式化分析。配对是 BLE 安全体系中的关键环节，决定了后续通信加密密钥的协商方式，因此其安全性直接影响设备间数据传输的机密性与完整性。作者构建了该协议的正式模型，通过验证脚本对协议逻辑进行严谨的数学推演，并实现了相应的攻击以验证理论发现。研究的核心贡献在于揭示了一种名为“PE 混淆攻击”（PE Confusion Attack）的新型安全威胁，该攻击利用协议中配对阶段参数（Pairing Element, PE）的语义歧义或验证缺失，可能导致攻击者混淆不同配对过程中的关键参数，进而削弱配对过程提供的安全保障。论文提供了完整的工件，包括模型、脚本和攻击实现，供后续研究者复现与深入分析。这项研究对于蓝牙协议栈实现者、安全审计人员以及物联网设备制造商具有重要参考价值，有助于理解 BLE 配对协议在形式化层面存在的设计缺陷，并为未来协议修订或补丁提供理论依据。本文仅基于论文摘要，具体攻击细节和技术路线尚未公开，但其揭示的协议漏洞方向值得关注。

比特币最近引入了V2 P2P传输协议，旨在加密节点间的通信，以防范已知的攻击向量。然而，本研究发现该协议的设计存在概念性缺陷（并非实现错误），且这些问题同样适用于其他P2P网络。攻击者可以通过TCP负载长度识别应用消息；利用加密通道的工作机制对目标节点发起日蚀攻击（eclipse attack），使其与网络隔离；还能通过兼容性设计机制将所有连接降级为未加密的旧协议。研究者通过网络测量、仿真和模拟验证了这些攻击的有效性，并提出了短期和长期的对策建议。这是首次在V2 P2P传输背景下对比特币安全性进行系统研究。

WCDCAnalyzer 是一篇针对 Wi-Fi 认证设备连接协议（WCDC）的可扩展安全分析论文。研究背景是 Wi-Fi 设备连接协议（如 Wi-Fi Easy Connect、Wi-Fi Direct 等）在智能家居、物联网等场景广泛应用，但现有的安全分析工具通常难以应对协议状态空间爆炸和认证流程复杂的问题。核心问题是如何高效、自动化地检测这些协议中的逻辑漏洞、认证绕过或密钥协商缺陷。论文提出的 WCDCAnalyzer 方法采用符号执行与模型检验结合的方式，将协议规范建模为有限状态机，并利用符号执行探索认证握手过程中的所有可能路径。通过引入抽象化技术和并行化搜索策略，实现了对大规模协议状态空间的可扩展分析。主要贡献包括：设计了一种基于协议规范自动生成安全属性的方法；实现了对 Wi-Fi Easy Connect 和 Wi-Fi Direct 协议的完整分析，发现了多个之前未知的漏洞，如未授权设备配对、中间人攻击风险等；实验表明 WCDCAnalyzer 能够在数小时内完成对复杂协议的分析，而传统方法需要数天。该工作为 Wi-Fi 设备互操作性认证中的安全评估提供了高效工具，适合协议开发者、安全测试人员和认证机构参考。

本文提出了SecGoal，这是首个由专家标注的基准测试，覆盖了15种广泛部署的协议文档，包括5G-AKA和TLS 1.3。同时，作者提出了AIFG（AI-assisted framework），一种将安全目标提取与形式化分解为上下文感知的目标提取和检索增强形式化的AI辅助框架。研究评估了当代大语言模型（LLM）自动化此流程的能力，发现前沿模型（如Gemini 2.5-Pro）召回率高但精确度低于15%，经常将操作文本误分类为安全目标。相反，在SecGoal上进行指令微调后，紧凑模型（7B/9B参数）的F1分数超过80%，显著优于更大的通用模型。本文为自动化形式化协议分析建立了基础数据集和可重复基线。