摘要： 从ECS1协议和PFH协议出发，研究三轮乐观合同签订协议的结构。利用协议动作序列及条件图建立协议模型，分析三轮协议满足有限性的条件。在此基础上，结合模型检测工具SPIN，对满足有限性的协议结构的公平性进行分析、验证，并给出反例，说明三轮协议不可能同时满足有限性和公平性。

关键词: 合同签订协议, 乐观, 模型检测, 公平性, 有限性

Abstract: This paper studies the various structures of three-round optimistic contract signing protocol. The protocol structures are modeled by protocol motion chart and the property of timeliness is analyzed. Getting the structures which meet the timeliness requirement, it further analyzes and verifies the fairness property. Counterexamples are given by the model checker SPIN. Result shows that three-round protocols can not achieve both the fairness and timeliness.

Key words: contract signing protocol, optimistic, model checking, fairness, timeliness

中图分类号: 

• TP309.2