Formal Analysis of a Fair Payment Protocol

J.G. Cederquist, M.T. Dashti

    Research output: Book/ReportReportOther research output

    73 Downloads (Pure)


    We formally specify a payment protocol. This protocol is intended for fair exchange of timesensitive 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.
    Original languageUndefined
    Place of PublicationAmsterdam, the Netherlands
    Publication statusPublished - 2004

    Publication series

    NameReport / CWI


    • IR-77048

    Cite this