USP Electronic Research Repository

Model checking a server - side micro payment protocol

Chaudhary, Kaylash C. and Fehnker, Ansgar (2015) Model checking a server - side micro payment protocol. In: Formal Methods for Industrial Critical Systems. Lecture Notes in Computer Science, 9128 . Springer International Publishing, Switzerland, pp. 96-110. ISBN 978-3-319-19457-8

[img]
Preview
PDF - Published Version
Download (238Kb) | Preview

    Abstract

    Many virtual payment systems are available on the world wide web for micropayment, and as they deal with money, correctness is important. One such payment system is Netpay. This paper examines the server-side version of the Netpay protocol and provides its formalization as a CSP model. The PAT model checker is used to prove three properties essential for correctness: impossibility of double spending, validity of an ecoin during the execution and the absence of deadlock. We prove that the protocol is executing according to its description based on the assumption that the customers and vendors are cooperative. This is a very strong assumption for system built to prevent abuse, but further analysis suggests that without it the protocol does no longer guarantee all correctness properties.

    Item Type: Book Chapter
    Additional Information: DOI: 10.1007/978-3-319-19458-5_7 This paper was presented at 20th International Workshop, FMICS 2015 Oslo, Norway, June 22-23, 2015 Proceedings
    Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
    Divisions: Faculty of Science, Technology and Environment (FSTE) > School of Computing, Information and Mathematical Sciences
    Depositing User: Kaylash Chaudhary
    Date Deposited: 05 May 2016 10:47
    Last Modified: 24 May 2016 12:28
    URI: http://repository.usp.ac.fj/id/eprint/8849
    UNSPECIFIED

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...