Formal Analysis of a Fair Payment Protocol

J.G. Cederquist, Muhammad Torabi Dashti

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publication2nd International Workshop on Formal Aspect of Security and Trust (FAST)
    EditorsTheo Dimitrakos, Fabio Martinelli
    Place of PublicationBoston, Massachusetts
    PublisherSpringer
    Pages41-54
    Number of pages14
    ISBN (Print)9780387240503
    DOIs
    Publication statusPublished - Aug 2004
    EventIFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust, FAST 2004 - Toulouse, France
    Duration: 22 Aug 200427 Aug 2004

    Publication series

    NameIFIP International Federation for Information Processing
    PublisherKluwer Academic Publishers
    Volume173
    ISSN (Print)1571-5736

    Workshop

    WorkshopIFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust, FAST 2004
    Abbreviated titleFAST
    CountryFrance
    CityToulouse
    Period22/08/0427/08/04

    Keywords

    • EWI-762
    • IR-48702
    • METIS-220417
    • SCS-Cybersecurity

    Cite this

    Cederquist, J. G., & Dashti, M. T. (2004). Formal Analysis of a Fair Payment Protocol. In T. Dimitrakos, & F. Martinelli (Eds.), 2nd International Workshop on Formal Aspect of Security and Trust (FAST) (pp. 41-54). (IFIP International Federation for Information Processing; Vol. 173). Boston, Massachusetts: Springer. https://doi.org/10.1007/0-387-24098-5_4
    Cederquist, J.G. ; Dashti, Muhammad Torabi. / Formal Analysis of a Fair Payment Protocol. 2nd International Workshop on Formal Aspect of Security and Trust (FAST). editor / Theo Dimitrakos ; Fabio Martinelli. Boston, Massachusetts : Springer, 2004. pp. 41-54 (IFIP International Federation for Information Processing).
    @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 = "8",
    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)",

    }

    Cederquist, JG & Dashti, MT 2004, Formal Analysis of a Fair Payment Protocol. in T Dimitrakos & F Martinelli (eds), 2nd International Workshop on Formal Aspect of Security and Trust (FAST). IFIP International Federation for Information Processing, vol. 173, Springer, Boston, Massachusetts, pp. 41-54, IFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust, FAST 2004, Toulouse, France, 22/08/04. https://doi.org/10.1007/0-387-24098-5_4

    Formal Analysis of a Fair Payment Protocol. / Cederquist, J.G.; Dashti, Muhammad Torabi.

    2nd International Workshop on Formal Aspect of Security and Trust (FAST). ed. / Theo Dimitrakos; Fabio Martinelli. Boston, Massachusetts : Springer, 2004. p. 41-54 (IFIP International Federation for Information Processing; Vol. 173).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - Formal Analysis of a Fair Payment Protocol

    AU - Cederquist, J.G.

    AU - Dashti, Muhammad Torabi

    PY - 2004/8

    Y1 - 2004/8

    N2 - 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.

    AB - 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.

    KW - EWI-762

    KW - IR-48702

    KW - METIS-220417

    KW - SCS-Cybersecurity

    U2 - 10.1007/0-387-24098-5_4

    DO - 10.1007/0-387-24098-5_4

    M3 - Conference contribution

    SN - 9780387240503

    T3 - IFIP International Federation for Information Processing

    SP - 41

    EP - 54

    BT - 2nd International Workshop on Formal Aspect of Security and Trust (FAST)

    A2 - Dimitrakos, Theo

    A2 - Martinelli, Fabio

    PB - Springer

    CY - Boston, Massachusetts

    ER -

    Cederquist JG, Dashti MT. Formal Analysis of a Fair Payment Protocol. In Dimitrakos T, Martinelli F, editors, 2nd International Workshop on Formal Aspect of Security and Trust (FAST). Boston, Massachusetts: Springer. 2004. p. 41-54. (IFIP International Federation for Information Processing). https://doi.org/10.1007/0-387-24098-5_4