公平交换协议形式逻辑

Formal Logic for Fair Exchange Protocols

在深入分析公平交换协议现有研究和各项安全属性的基础上,由于信任逻辑方法难以分析乐观公平交换协议的公平性和时限性,提出一种公平交换协议形式化模型和推理逻辑.新模型将信道错误转化为攻击行为,将参与者分为诚实与不诚实两类,并将这些威胁归结为两类入侵者.基于模型检查思想,新逻辑将协议定义为Kripke结构的演化系统,将参与者看作异步环境中的通信进程,定义了时间算子控制实体行为的转换.同时,新逻辑继承了信任逻辑简单、实用的优点.以一个典型协议为例,采用逻辑结合模型检查的方法,演示了分析协议的过程.发现并改进了协议实例的安全缺陷.案例分析表明,新逻辑能够分析公平交换协议的公平性和时限性.

The fairness and punctuality of optimistic fair exchange protocols are difficult to analyze by using belief logic. Based on the studies of existing formal models and security attributes in fair exchange, a formal model for logic reasoning and fair exchange protocols is proposed. In the model, the channel errors are transferred to the attacker＇s behaviors, the participants are divided into honest and dishonest ones, and the threats are attributed to two types of intruders. Based on the idea of model checking, the protocols are defined as an evolved system that has the Kripke structure, and the parties are considered as processes in an asynchronous environment. The new logic stimulates the time operators to control the transfers among the participants＇ behaviors and is simple and easy to use. Through typical optimistic fair exchange protocols, the article demonstrates the course of protocol analysis. Two flaws of the protocol are discovered and improved. The case study shows that the new logic can be used to analyze the fairness and timeliness of fair exchange nrotocols.