Game analysis of abuse-free contract signing

In this paper we report on the verification of two contract signing protocols. Our verification method is based on the idea of modeling those protocols as games, and reasoning about their properties as strategies for players. We use the formal model of alternating transition systems to represent the protocols and alternating-time temporal logic to specify properties. The paper focuses on the verification of abuse-freeness, relates this property to the balance property, previously studied using two other formalisms, shows some ambiguities in the definition of abuse-freeness and proposes a new, stronger definition. Formal methods are not only useful here to verify automatically the protocols but also to better understand their requirements (balance and abuse-freeness are quite complicated and subtle properties).