Modelling a Java Ring based implementation of an N-Count payment system

J.D. Revill, Pieter H. Hartel

    Abstract

    N-Count is a system for offline value transfer. A prototype of an N-Count payment system has been designed, and it has been implemented in Java. We have used the Java Ring with the Java Card API as a secure device. The system has also been modelled using the Spin model checker. The combined prototyping and model checking has made it possible to investigate safety properties of the prototype, both formally and intuitively. Because of this model building activity, problems have been identified and solved before an actual system has been built.
    Original languageUndefined
    Pages139-150
    Number of pages12
    StatePublished - Sep 1999

    Fingerprint

    Model checking
    Application programming interfaces (API)

    Keywords

    • SCS-Cybersecurity
    • IR-55687
    • EWI-1030

    Cite this

    Revill, J.D.; Hartel, Pieter H. / Modelling a Java Ring based implementation of an N-Count payment system.

    1999. 139-150.

    Research output: Scientific - peer-reviewPaper

    @misc{c7b1c3a8fbcf42718cf7fe1392ea2cb7,
    title = "Modelling a Java Ring based implementation of an N-Count payment system",
    abstract = "N-Count is a system for offline value transfer. A prototype of an N-Count payment system has been designed, and it has been implemented in Java. We have used the Java Ring with the Java Card API as a secure device. The system has also been modelled using the Spin model checker. The combined prototyping and model checking has made it possible to investigate safety properties of the prototype, both formally and intuitively. Because of this model building activity, problems have been identified and solved before an actual system has been built.",
    keywords = "SCS-Cybersecurity, IR-55687, EWI-1030",
    author = "J.D. Revill and Hartel, {Pieter H.}",
    note = "Imported from DIES",
    year = "1999",
    month = "9",
    pages = "139--150",

    }

    Modelling a Java Ring based implementation of an N-Count payment system. / Revill, J.D.; Hartel, Pieter H.

    1999. 139-150.

    Research output: Scientific - peer-reviewPaper

    TY - CONF

    T1 - Modelling a Java Ring based implementation of an N-Count payment system

    AU - Revill,J.D.

    AU - Hartel,Pieter H.

    N1 - Imported from DIES

    PY - 1999/9

    Y1 - 1999/9

    N2 - N-Count is a system for offline value transfer. A prototype of an N-Count payment system has been designed, and it has been implemented in Java. We have used the Java Ring with the Java Card API as a secure device. The system has also been modelled using the Spin model checker. The combined prototyping and model checking has made it possible to investigate safety properties of the prototype, both formally and intuitively. Because of this model building activity, problems have been identified and solved before an actual system has been built.

    AB - N-Count is a system for offline value transfer. A prototype of an N-Count payment system has been designed, and it has been implemented in Java. We have used the Java Ring with the Java Card API as a secure device. The system has also been modelled using the Spin model checker. The combined prototyping and model checking has made it possible to investigate safety properties of the prototype, both formally and intuitively. Because of this model building activity, problems have been identified and solved before an actual system has been built.

    KW - SCS-Cybersecurity

    KW - IR-55687

    KW - EWI-1030

    M3 - Paper

    SP - 139

    EP - 150

    ER -