Title :
Game analysis of abuse-free contract signing
Author :
Kremer, Steve ; Raskin, Jean-Francois
Author_Institution :
Departement d´´Informatique, Univ. Libre de Bruxelles, Brussels, Belgium
Abstract :
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).
Keywords :
formal verification; game theory; protocols; temporal logic; abuse-free contract signing; alternating transition systems; alternating-time temporal logic; balance property; contract signing protocols verification; formal methods; formal model; game analysis; reasoning; subtle properties; Computer security; Conferences; Electronic commerce; Electronic mail; Forward contracts; Logic; Protocols; Waste materials;
Conference_Titel :
Computer Security Foundations Workshop, 2002. Proceedings. 15th IEEE
Print_ISBN :
0-7695-1689-0
DOI :
10.1109/CSFW.2002.1021817