We formally specify a payment protocol described by Vogt et al. This protocol is intended for fair exchange of time-sensitive data. Here the mCRL language is used to formalize the protocol. Fair exchange properties are expressed in the regular alternation-free mu-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.
|Name||IFIP International Federation for Information Processing|
|Publisher||Kluwer Academic Publishers|
|Workshop||IFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust, FAST 2004|
|Period||22/08/04 → 27/08/04|