DocumentCode
3129469
Title
Formal analysis of multi-party contract signing
Author
Chadha, Rohit ; Kramer, S. ; Scedrov, Andre
Author_Institution
Sussex Univ., London, UK
fYear
2004
fDate
28-30 June 2004
Firstpage
266
Lastpage
279
Abstract
We analyze the multi-party contract-signing protocols of Garay and MacKenzie (GM) and of Baum and Waidner (BW). We use a finite-state tool, MOCHA, which allows specification of protocol properties in a branching-time temporal logic with game semantics. While our analysis does not reveal any errors in the BW protocol, in the GM protocol we discover serious problems with fairness for four signers and an oversight regarding abuse-freeness for three signers. We propose a complete revision of the GM subprotocols in order to restore fairness.
Keywords
contracts; digital signatures; formal verification; protocols; temporal logic; Baum-Waidner protocol; Garay-MacKenzie protocol; Garay-MacKenzie subprotocols; MOCHA; abuse-freeness; fairness restoration; finite-state tool; formal analysis; game semantics; multiparty contract-signing protocols; temporal logic; Computer networks; Contracts; Electronic mail; Error correction; Logic; Protection; Protocols; Waste materials;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE
ISSN
1063-6900
Print_ISBN
0-7695-2169-X
Type
conf
DOI
10.1109/CSFW.2004.1310746
Filename
1310746
Link To Document