Optimistic contract signing protocols may involve subproto-cols that allow a contract to be signed normally or aborted or resolved by a third party. Since there are many ways these subprotocols might interact, protocol analysis involves consideration of a number of complicated cases. With the help of Murψ, a finite-state verification tool, we analyze the abuse-free optimistic contract signing protocol of Garay, Jakobsson, and MacKenzie. In addition to verifying a number of subtle properties, we discover an attack in which negligence or corruption of the trusted third party may allow abuse or unfairness. Contrary to the intent of the protocol, the cheated party is not able to hold the third party accountable. In addition to analyzing a modification to the protocol that avoids these problems, we discuss issues involved in the application of finite-state analysis to fair exchange protocols, in particular models of fairness guarantees, abuse, and corrupt protocol participants.
展开▼
