-
题名基于时间-事件逻辑的ID-AOFE协议形式化分析
- 1
-
-
作者
肖美华
乔珊珊
杨科
-
机构
华东交通大学信息与软件工程学院
-
出处
《郑州大学学报(理学版)》
北大核心
2026年第2期48-54,共7页
-
基金
国家自然科学基金项目(62362033,61962020)
江西省“双千人才”项目(JXSQ2023201009)
江西省自然科学基金重点项目(20224ACB202006)。
-
文摘
公平交换协议旨在为数字信息交换提供安全、公平的机制,分析该类协议的公平性是信息安全领域中一个重要的研究内容。时间-事件逻辑具有描述协议主体知识和状态随时间变化的机制,是一种分析协议安全属性的有效方法。基于时间-事件逻辑针对公平交换协议中主体互不信任、存在欺骗行为的特点,通过分析当协议结束运行时,是否存在使不诚实主体获得额外优势的策略来分析协议的公平性。以一个基于身份的混淆乐观公平交换(identity based-ambiguous optimistic fair exchange,ID-AOFE)协议为例进行分析,定义了一种规范的消息交互过程,对ID-AOFE协议消息交互过程中的时间进行了细粒度分析,发现协议中存在两个公平性漏洞,结合图形描述方式给出了攻击发生的全过程,说明了时间-事件逻辑理论的有效性。
-
关键词
形式化方法
时间事件逻辑
ID-AOFE协议
公平性分析
-
Keywords
formal method
t-loet
ID-AOFE protocol
fairness analysis
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
