Model Checking a Client-Side Micro Payment Protocol

Kaylash Chaudhary, Ansgar Fehnker

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

Abstract

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)
PublisherIEEE
Pages90-97
Number of pages8
ISBN (Electronic)978-1-5090-5753-5
ISBN (Print)978-1-5090-5754-2
DOIs
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

Conference

Conference3rd Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2016
Abbreviated titleAPWC on CSE
CountryFiji
CityNadi
Period5/12/166/12/16

Fingerprint

Model checking
Network protocols
Costs
Processing

Keywords

  • 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

Cite this

Chaudhary, K., & Fehnker, A. (2016). Model Checking a Client-Side Micro Payment Protocol. In 3rd Asia-Pacific World Congress on Computer Science and Engineering (APWC on CSE 2016) (pp. 90-97). IEEE. https://doi.org/10.1109/APWC-on-CSE.2016.026
Chaudhary, Kaylash ; Fehnker, Ansgar . / Model Checking a Client-Side Micro Payment Protocol. 3rd Asia-Pacific World Congress on Computer Science and Engineering (APWC on CSE 2016). IEEE, 2016. pp. 90-97
@inproceedings{840bfbf36b3940eba3b9b4521e0b08ea,
title = "Model Checking a Client-Side Micro Payment Protocol",
abstract = "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.",
keywords = "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",
author = "Kaylash Chaudhary and Ansgar Fehnker",
year = "2016",
month = "12",
day = "1",
doi = "10.1109/APWC-on-CSE.2016.026",
language = "English",
isbn = "978-1-5090-5754-2",
pages = "90--97",
booktitle = "3rd Asia-Pacific World Congress on Computer Science and Engineering (APWC on CSE 2016)",
publisher = "IEEE",
address = "United States",

}

Chaudhary, K & Fehnker, A 2016, Model Checking a Client-Side Micro Payment Protocol. in 3rd Asia-Pacific World Congress on Computer Science and Engineering (APWC on CSE 2016). IEEE, pp. 90-97, 3rd Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2016, Nadi, Fiji, 5/12/16. https://doi.org/10.1109/APWC-on-CSE.2016.026

Model Checking a Client-Side Micro Payment Protocol. / Chaudhary, Kaylash; Fehnker, Ansgar .

3rd Asia-Pacific World Congress on Computer Science and Engineering (APWC on CSE 2016). IEEE, 2016. p. 90-97.

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

TY - GEN

T1 - Model Checking a Client-Side Micro Payment Protocol

AU - Chaudhary, Kaylash

AU - Fehnker, Ansgar

PY - 2016/12/1

Y1 - 2016/12/1

N2 - 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.

AB - 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.

KW - electronic money

KW - formal verification

KW - CSP model

KW - Netpay protocol

KW - PAT model checker

KW - client-side micro payment protocol

KW - correctness checking

KW - credit card

KW - e-commerce

KW - micropayment systems

KW - model checking

KW - online payment

KW - virtual payment systems

KW - Credit cards

KW - Indexes

KW - Model checking

KW - Protocols

KW - Reactive power

KW - Tools

KW - Micropayment

KW - Model

KW - Verification

U2 - 10.1109/APWC-on-CSE.2016.026

DO - 10.1109/APWC-on-CSE.2016.026

M3 - Conference contribution

SN - 978-1-5090-5754-2

SP - 90

EP - 97

BT - 3rd Asia-Pacific World Congress on Computer Science and Engineering (APWC on CSE 2016)

PB - IEEE

ER -

Chaudhary K, Fehnker A. Model Checking a Client-Side Micro Payment Protocol. In 3rd Asia-Pacific World Congress on Computer Science and Engineering (APWC on CSE 2016). IEEE. 2016. p. 90-97 https://doi.org/10.1109/APWC-on-CSE.2016.026