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.
|Title of host publication||Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014|
|Publication status||Published - 5 Mar 2015|
|Event||Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014 - Nadi, Fiji|
Duration: 4 Nov 2014 → 5 Nov 2014
|Conference||Asia-Pacific World Congress on Computer Science and Engineering, APWC on CSE 2014|
|Abbreviated title||APWC on CSE 2014|
|Period||4/11/14 → 5/11/14|