Game-Based Analysis and Improvement of a Fair Contract Signing Protocol

Traditional temporal logic regards protocols as close system to analyze. In order to overcome the shortcoming of traditional temporal logic, an game-based analysis method is inducted. This method is applied to formal analyze a fair contract signing protocol, and then some defects of the protocol are found. An improvement protocol is proposed which fixes the flaw by adding some extra time limit information and an abort sub-protocol. The fairness and the timeliness of the improvement protocol are validated by ATL formula and Invariant Checking. It is found that the improvement protocol satisfies the timeliness and the fairness.