公平交换协议的信道可信度形式化验证方法

Formal Verification Method for Fair Exchange Protocol by Channel Credibility

公平交换协议是一种重要的电子商务安全协议,已有的针对公平交换协议进行的形式化验证只能定性分析协议是否满足给定性质,本文提出基于信道可信度的公平交换协议的形式化验证方法,重点对信道问题进行定量分析.以一个电子合同签署协议为例,通过概率模型检测的方法对协议建立离散时间马尔可夫链模型,用概率计算树逻辑对协议属性进行描述,通过PRISM概率模型检测工具对协议进行定量的验证和分析.实验结果表明公平交换协议各实体间信道可信度对协议的公平性、有效性和时限性有不同程度的影响,对相应信道进行控制或改善可以提高协议安全性.

Fair exchange protocol is an important e-commerce security protocol.The existing formal verification for the fair exchange protocol can only qualitatively analyze whether the protocol satisfies the given property.This paper presents a formal verification method for fair exchange protocol based on channel confidenceand focus on the quantitative analysis of channel problems.Taking an electronic contract signing protocol as an example,this paper establishes the discrete-time Markov Chain for the protocol by probabilistic model detection method,describes the attribute of the protocol by probabilistic computation tree logic,verifies the protocol quantitatively by PRISM probabilistic model checking tool.Experimental results show that the channel reliability of the entities of the fair exchange protocol has different influence on the fairness,effectiveness and timeliness of the protocol.Control or improvement of the corresponding channel can improve protocol security.