计算机工程2011，Vol.37Issue(7)：142-144,147,4.DOI:10.3969/j.issn.1000-3428.2011.07.047
乐观合同签订协议的模型检测分析
Model Checking Analysis of Optimistic Contract Signing Protocol
摘要
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分类
信息技术与安全科学引用本文复制引用
周立青,杨晋吉..乐观合同签订协议的模型检测分析[J].计算机工程,2011,37(7):142-144,147,4.基金项目
国家"973"计划基金资助项目(2009CB320701) （2009CB320701）
广东省科技计划基金资助项目(2007B010400068) （2007B010400068）
