Formal Analysis of Multiparty Contract Signing |
| |
| Authors: | Rohit Chadha Steve Kremer Andre Scedrov |
| |
| Affiliation: | (1) University of Sussex, Sussex, UK;(2) Laboratoire Spécification et Vérification, CNRS, UMR 8643, INRIA Futurs Projet SECSI & école Normale Supérieure de Cachan, 61, avenue du Président Wilson, 94235 Cachan Cedex, France;(3) University of Pennsylvania, Philadelphia, PA, USA |
| |
| Abstract: | We analyze the multiparty 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: | multiparty contract signing GM protocol |
| 本文献已被 SpringerLink 等数据库收录！ |
|
