Formal Analysis of a Fair Payment Protocol

We formally specify a payment protocol described in [Vogt et al., 2001]. This protocol is intended for fair exchange of time-sensitive data. Here the µCRL language is used to formalize the protocol. Fair exchange properties are expressed in the regular alternation-free µ-calculus. These properties are then verified using the finite state model checker from the CADP toolset. Proving fairness without resilient communication channels is impossible. We use the Dolev-Yao intruder, but since the conventional Dolev-Yao intruder violates this assumption, it is forced to comply to the resilient communication channel assumption.

• Type: Conference
• Year: 2004
• Where: IFIP
• Authors: Jan Cederquist, Muhammad Torabi Dashti
• Keywords: Communications, Dolev-Yao Intruder, Fair Exchange, IFIP 2004, Resilient Communication Channel