基于时间-事件逻辑的ID-AOFE协议形式化分析OA

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.