Analysis of a Fair Exchange Protocol

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.

• Type: Conference
• Year: 2000
• Where: NDSS
• Authors: Vitaly Shmatikov, John C. Mitchell
• Keywords: Computer Networks, Contract Signing Protocol, Fair Exchange Protocols, NDSS 2000, finitestate Analysis Tool