Date Added: Oct 2009
A Multi-Party Contract Signing (MPCS) protocol is used for a group of signers to sign a digital contract over a network. The authors analyze the protocols of Mukhamedov and Ryan (MR), and of Mauw, Radomirovi?c and Torabi Dashti (MRT), using the finite-state model checker Mocha. Mocha allows for the specification of properties in Alternating-time Temporal Logic (ATL) with game semantics, and the model checking problem for ATL requires the computation of winning strategies. This gives them an intuitive interpretation of the verification problem of crucial properties of MPCS protocols. They analyze the MR protocol with up to 5 signers and their analysis does not reveal any flaws. MRT protocols can be generated from minimal message sequences, depending on the number of signers.