Formal Analysis of a Fair Payment Protocol

J.G. Cederquist, M.T. Dashti

    Research output: Book/Report › Report › Other research output

    73 Downloads (Pure)

    Abstract

    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
    PublisherC.W.I.
    Publication statusPublished - 2004

    Publication series

    NameReport / CWI
    PublisherCWI
    VolumeSEN-Ro

    Keywords

    • IR-77048

    Access to Document

      Cite this