郑州大学学报（理学版）2026，Vol.58Issue(2)：48-54,7.DOI:10.13705/j.issn.1671-6841.2024143
基于时间-事件逻辑的ID-AOFE协议形式化分析
Formal Analysis of ID-AOFE Protocol Based on Time-event Logic
摘要
Abstract
Fair exchange protocols aimed at providing a secure and fair mechanism for digital information exchange.Analyzing the fairness of such protocols was an important research content in the field of infor-mation security.Time-event logic had a mechanism to describe the knowledge and state changes of proto-col subjects over time and was considered an effective method for analyzing the security attributes of proto-cols.Based on time-event logic,in view of the characteristics of mutual distrust and deceptive behaviors in fair exchange protocols,the fairness of the protocol was analyzed by determining whether there was a strategy that could enable dishonest subjects to gain additional advantages when the protocol ended its op-eration.An example was analized by using an identity based-ambiguous optimistic fair exchange(ID-AOFE)protocol.A standardized message interaction process was defined.A fine-grained analysis of the time in the message interaction process of the protocol was conducted.Two fairness loopholes in the pro-tocol were discovered.The entire process of the attack occurrence was given in combination with the graphical description method,illustrating the validity of the theory.关键词
形式化方法/时间事件逻辑/ID-AOFE协议/公平性分析Key words
formal method/T-LoET/ID-AOFE protocol/fairness analysis分类
信息技术与安全科学引用本文复制引用
肖美华,乔珊珊,杨科..基于时间-事件逻辑的ID-AOFE协议形式化分析[J].郑州大学学报（理学版）,2026,58(2):48-54,7.基金项目
国家自然科学基金项目(62362033,61962020) （62362033,61962020）
江西省"双千人才"项目(JXSQ2023201009) （JXSQ2023201009）
江西省自然科学基金重点项目(20224ACB202006) （20224ACB202006）
