We formally specify a payment protocol. 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.

Specification and verification (program logics, model checking, etc.) (msc 68Q60), Network protocols (msc 68M12), Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (msc 68N30)
CWI
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

Cederquist, J.G, & Dashti, M.T. (2004). Formal analysis of a fair payment protocol. Software Engineering [SEN]. CWI.