Analysis of a Fair Exchange Protocol.
Vitaly Shmatikov, John C. Mitchell · 2000
We analyze an optimistic contract signing protocol of Asokan, Shoup, and Waidner as a case study in the applicability of formal methods to verification of fair exchange protocols. After discussing the challenges involved in formalizing fairness, we use Mur', a finitestate analysis tool, to discover a weakness in the protocol that enables a malicious participant to produce inconsistent versions of the contract or mount a replay attack. We show that the protocol can be repaired, and that the confidentiality assumption about the communication channels may be relaxed while preserving security against the conventional Dolev-Yao intruder. 1. Introduction With continuing growth of electronic commerce on the Internet, the issues of trust and fairness are becoming increasingly important. The current proliferation of online auction venues, Internet shopping malls, and other sites that act as brokers between individual users and/or commercial entities makes it difficult, if not altogether infea...