%0 Journal Article %A Kaylash Chaudhary and Ansgar Fehnker %D 2012 %J International Journal of Mathematical and Computational Sciences %B World Academy of Science, Engineering and Technology %I Open Science Index 72, 2012 %T Modeling and Verification for the Micropayment Protocol Netpay %U https://publications.waset.org/pdf/5912 %V 72 %X There are many virtual payment systems available to conduct micropayments. It is essential that the protocols satisfy the highest standards of correctness. This paper examines the Netpay Protocol [3], provide its formalization as automata model, and prove two important correctness properties, namely absence of deadlock and validity of an ecoin during the execution of the protocol. This paper assumes a cooperative customer and will prove that the protocol is executing according to its description. %P 1718 - 1726