Formal Analysis of a Fair Payment Protocol

J.G. Cederquist, Muhammad Torabi Dashti

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

    2 Citations (Scopus)
    6 Downloads (Pure)


    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
    Number of pages14
    ISBN (Print)9780387240503
    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
    ISSN (Print)1571-5736


    WorkshopIFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust, FAST 2004
    Abbreviated titleFAST


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

    Cite this