Model Checking a Client-Side Micro Payment Protocol

Kaylash Chaudhary, Ansgar Fehnker

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

    5 Downloads (Pure)


    Virtual payment systems overcome the drawbacks such as processing and operational cost of the traditional payment system. The main aim of the virtual payment system is to provide efficient services in terms of cost. Online payment using credit card is one of the most expensive of all payment means. This gives advantage to micropayment systems where only small amounts are used for e-commerce. Payment which are small will be costly if paid through credit card. Therefore, there are several micropayment systems that exist and some have been proposed. One of the proposed micropayment system that this paper will talk about is Netpay. We will do model checking to check the correctness of this payment system and to see whether the protocol designers property claim is valid. Correctness is important in payment systems because money is involved in it, therefore the protocol needs to be validated. This paper examines the client-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. We compare the two variation of the protocol with each other and with the properties claimed by the protocol designers.
    Original languageEnglish
    Title of host publication3rd Asia-Pacific World Congress on Computer Science and Engineering (APWC on CSE 2016)
    Number of pages8
    ISBN (Electronic)978-1-5090-5753-5
    ISBN (Print)978-1-5090-5754-2
    Publication statusPublished - 1 Dec 2016
    Event3rd Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2016 - Nadi, Fiji
    Duration: 5 Dec 20166 Dec 2016
    Conference number: 3


    Conference3rd Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2016
    Abbreviated titleAPWC on CSE


    • electronic money
    • formal verification
    • CSP model
    • Netpay protocol
    • PAT model checker
    • client-side micro payment protocol
    • correctness checking
    • credit card
    • e-commerce
    • micropayment systems
    • model checking
    • online payment
    • virtual payment systems
    • Credit cards
    • Indexes
    • Model checking
    • Protocols
    • Reactive power
    • Tools
    • Micropayment
    • Model
    • Verification


    Dive into the research topics of 'Model Checking a Client-Side Micro Payment Protocol'. Together they form a unique fingerprint.

    Cite this