Formal Analysis of a Fair Payment Protocol


Share/Save/Bookmark

Cederquist, Jan and Dashti, Muhammad Torabi (2005) Formal Analysis of a Fair Payment Protocol. In: IFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust (FAST), World Computer Congress, August 22-27, 2004, Toulouse, France (pp. pp. 41-54).

[img] PDF
Restricted to UT campus only
: Request a copy
765kB
Abstract: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.
Item Type:Conference or Workshop Item
Copyright:© 2005 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/48702
Official URL:http://dx.doi.org/10.1007/0-387-24098-5_4
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 220417