Modeling and verification for the server-side Netpay protocol

Kaylash Chaudhary; Ansgar Fehnker; Xiaoling Dai

doi:10.1109/APWCCSE.2014.7053852

Modeling and verification for the server-side Netpay protocol

Kaylash Chaudhary, Ansgar Fehnker, Xiaoling Dai

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Abstract

Many virtual payment systems are available on the world wide web for micropayment. Correctness is important for these payment systems as it deals with money. One such payment system is Netpay. This paper examines the server-side Netpay protocol and provides its formalization as an interface automata model to prove three properties which are double spending, validity of an ecoin location and the absence of the deadlock. We will prove that the protocol is executing according to its description based on the assumption that the customers and vendors are cooperative.

Original language	English
Title of host publication	Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014
Publisher	IEEE
ISBN (Electronic)	9781479919550
DOIs	https://doi.org/10.1109/APWCCSE.2014.7053852
Publication status	Published - 5 Mar 2015
Externally published	Yes
Event	Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014 - Nadi, Fiji Duration: 4 Nov 2014 → 5 Nov 2014

Conference

Conference	Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014
Abbreviated title	APWC on CSE 2014
Country/Territory	Fiji
City	Nadi
Period	4/11/14 → 5/11/14

Keywords

micropayment
Model
verification

Access to Document

10.1109/APWCCSE.2014.7053852

Cite this

@inproceedings{989298ea14a84e1c9cf7aafbedcdbca0,

title = "Modeling and verification for the server-side Netpay protocol",

abstract = "Many virtual payment systems are available on the world wide web for micropayment. Correctness is important for these payment systems as it deals with money. One such payment system is Netpay. This paper examines the server-side Netpay protocol and provides its formalization as an interface automata model to prove three properties which are double spending, validity of an ecoin location and the absence of the deadlock. We will prove that the protocol is executing according to its description based on the assumption that the customers and vendors are cooperative.",

keywords = "micropayment, Model, verification",

author = "Kaylash Chaudhary and Ansgar Fehnker and Xiaoling Dai",

note = "Publisher Copyright: {\textcopyright} 2014 IEEE.; Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014, APWC on CSE 2014 ; Conference date: 04-11-2014 Through 05-11-2014",

year = "2015",

month = mar,

day = "5",

doi = "10.1109/APWCCSE.2014.7053852",

language = "English",

booktitle = "Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014",

publisher = "IEEE",

address = "United States",

}

TY - GEN

T1 - Modeling and verification for the server-side Netpay protocol

AU - Chaudhary, Kaylash

AU - Fehnker, Ansgar

AU - Dai, Xiaoling

PY - 2015/3/5

Y1 - 2015/3/5

N2 - Many virtual payment systems are available on the world wide web for micropayment. Correctness is important for these payment systems as it deals with money. One such payment system is Netpay. This paper examines the server-side Netpay protocol and provides its formalization as an interface automata model to prove three properties which are double spending, validity of an ecoin location and the absence of the deadlock. We will prove that the protocol is executing according to its description based on the assumption that the customers and vendors are cooperative.

AB - Many virtual payment systems are available on the world wide web for micropayment. Correctness is important for these payment systems as it deals with money. One such payment system is Netpay. This paper examines the server-side Netpay protocol and provides its formalization as an interface automata model to prove three properties which are double spending, validity of an ecoin location and the absence of the deadlock. We will prove that the protocol is executing according to its description based on the assumption that the customers and vendors are cooperative.

KW - micropayment

KW - Model

KW - verification

UR - http://www.scopus.com/inward/record.url?scp=84988214316&partnerID=8YFLogxK

U2 - 10.1109/APWCCSE.2014.7053852

DO - 10.1109/APWCCSE.2014.7053852

M3 - Conference contribution

AN - SCOPUS:84988214316

BT - Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014

PB - IEEE

T2 - Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014

Y2 - 4 November 2014 through 5 November 2014

ER -

Modeling and verification for the server-side Netpay protocol

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this