Model Checking Analysis of Optimistic Contract Signing Protocol
Jinji Yang · Jisuanji gongcheng · 2011
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.