新刊速递|华东交通大学信息与软件工程学院肖美华教授团队:基于时间-事件逻辑的ID-AOFE协议形式化分析

华东交通大学信息与软件工程学院肖美华教授团队在《郑州大学学报(理学版)》上发表题为：“基于时间-事件逻辑的ID-AOFE协议形式化分析”的研究型论文。

Cite: XIAO Meihua, QIAO Shanshan, YANG Ke. Formal Analysis of ID-AOFE Protocol Based on Time-event Logic[J]. Journal of Zhengzhou University(Natural Science Edition), 2026, 58(2): 48-54.

互联网已深度融入社会生活，安全协议作为保障网络通信安全的关键技术，其正确性与可靠性至关重要。公平交换协议是安全协议的一种，旨在确保协议中的其他主体不能获得比诚实主体更多的利益，广泛应用于电子合同签署、电子商务和安全消息传递等场景。

形式化方法为安全协议的严谨分析提供了数学基础，主要包括定理证明与模型检测两类。其中，定理证明方法不受系统状态空间限制，具有高度的严谨性与精确性；事件逻辑作为定理证明的一种有效工具，能够对协议执行过程及其安全目标进行精确建模与形式化描述，显著降低协议分析的复杂性。

然而，现有研究在刻画时间因素对协议安全性的影响方面仍显不足。安全协议中消息的发送、接收及有效性往往依赖于严格的时间约束，忽略时间维度可能导致对公平性等关键属性的误判。尽管已有工作尝试引入时间相关逻辑或博弈模型分析协议公平性，但在对协议整体执行过程、时限机制与信道行为的综合建模上仍存在局限。

本文针对基于身份的混淆乐观公平交换协议（identity based-ambiguous optimistic fair exchange,ID-AOFE），将时间因素系统引入事件逻辑框架，通过构建时间-事件耦合的形式化模型，深入分析不同主体行为下协议的公平性保障能力。该研究不仅有助于揭示协议潜在的安全缺陷，也为时限敏感型安全协议的验证提供了可扩展的理论方法。

本文首先基于时间-事件逻辑对身份认证的混淆乐观公平方案（ID-AOFE）协议进行形式化建模，定义主体在各时刻的知识集、消息发送/接收动作及加密操作，并引入时间参数 T 刻画争端解决时限。随后，分别从发起者为恶意和响应者为恶意两种场景展开分析。

当发起者（Alice）为恶意时，其可在收到响应者（Bob）的完整签名后拒绝发送自身签名，并进一步阻断Bob与TTP之间的通信。由于TTP仅在时限 T 内处理请求，Bob因超时无法获得救济，处于不公平状态。当响应者（Bob）为恶意时，其可向Alice发送未经验证的虚假完整签名，而协议未提供完整签名验证算法，导致Alice误以为交换完成，实际却未获得有效签名。

分析表明，这两个漏洞均源于协议对时间边界与消息真实性的保障不足。本文加入了时间因素的事件逻辑理论分析基于身份的混淆乐观公平协议(ID-AOFE)，并形式化建模需要满足的安全属性，形式化模型准确、完整地刻画了ID-AOFE协议的流程，并检验出该协议存在两个攻击漏洞以及不公平性，说明了加入时间因素的事件逻辑方法在分析协议公平性上是通用且可行的。本模型具有很好的扩展性, 这种时间细粒度建模方法同样也适用于类似的公平性交换协议，有助于发现协议交互过程中隐藏的时限性攻击。在以后的工作中将继续添加其他定理证明因素，使构建的验证平台能够更加快捷高效地证明网络协议的安全性。

图1 ID-AOFE协议方案的信息交互模型。该图展示Alice与Bob在无争议情况下的标准交换流程：Alice先发部分签名，Bob验证后回传完整签名，Alice再发送自身完整签名，双方最终均获得所需信息。

图2 响应者发起争端请求。 该图展示了当Alice违约时，Bob在时限 T 内向TTP提交证据，TTP验证后返回Alice的完整签名。该图凸显时限 T 的关键作用——若通信被恶意阻断导致超时，争端机制失效。

图3 发起者发起争端请求。 该图展示当Bob未响应时，Alice在 t>T 后请求TTP介入，TTP依据历史记录决定是否发放Bob的签名。此流程依赖数据库完整性，但无法防范图2中的主动阻断攻击。

图4 发起者为恶意主体时的时限性缺陷。展示清晰刻画攻击全过程：Alice发送部分签名 → Bob回传完整签名 → Alice不回应并阻断Bob-TTP链路 → Bob请求超时 → 协议终止且Bob未获签名，构成典型不公平场景。

扫描上方二维码，或点击文末“阅读原文”查看文献。

https://html.rhhz.net/ZZDXXBLXB/html/20260207.htm

郑州大学学报（理学版）

《郑州大学学报（理学版）》是郑州大学主办的自然科学类综合性学术刊物。主要刊登信息与计算机科学、数学、物理学、化学、生物工程科学、材料科学与电气工程科学等自然科学各学科的基础研究及应用研究方面的学术论文。本刊所发表的论文已被《中国数学文摘》、《中国物理文摘》、荷兰《Scopus数据库》、美国《数学评论》、俄罗斯《文摘杂志》及波兰《哥白尼索引》等国内外多家权威文摘杂志及数据库收录或评论，致力于促进自然科学领域的学术交流与发展。