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

摘要

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