@inproceedings{7b7fabd21cb241098ed8addc6a7e61bb,
title = "Formal Analysis of a Fair Payment Protocol",
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.",
keywords = "EWI-762, IR-48702, METIS-220417, SCS-Cybersecurity",
author = "J.G. Cederquist and Dashti, \{Muhammad Torabi\}",
year = "2004",
month = aug,
doi = "10.1007/0-387-24098-5\_4",
language = "English",
isbn = "9780387240503",
series = "IFIP International Federation for Information Processing",
publisher = "Springer",
pages = "41--54",
editor = "Theo Dimitrakos and Fabio Martinelli",
booktitle = "2nd International Workshop on Formal Aspect of Security and Trust (FAST)",
address = "Germany",
note = "IFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust, FAST 2004, FAST ; Conference date: 22-08-2004 Through 27-08-2004",
}