Formal analysis of a fair payment protocol
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)|
|Software Engineering [SEN]|
|Organisation||Specification and Analysis of Embedded Systems|
Cederquist, J.G, & Dashti, M.T. (2004). Formal analysis of a fair payment protocol. Software Engineering [SEN]. CWI.