论文部分内容阅读
公平交换协议的结构常常比较复杂，可能由多个子协议组合而成，并不一定按顺序结构执行协议。因此，公平交换协议的公平性分析需要选择适宜的形式化方法。扩展了串空间逻辑，利用扩展后的串空间轨迹图分析了在线TTP类型协议的公平性；利用扩展的发送边和主动测试定理，对离线TTP类型协议的公平性进行了分析，分别提供了具有可信第三方参与的两种主要类型的公平交换协议公平性的形式化分析方法。