@article{(Open Science Index):https://publications.waset.org/pdf/5912, title = {Modeling and Verification for the Micropayment Protocol Netpay}, author = {Kaylash Chaudhary and Ansgar Fehnker}, country = {}, institution = {}, abstract = {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.}, journal = {International Journal of Mathematical and Computational Sciences}, volume = {6}, number = {12}, year = {2012}, pages = {1718 - 1726}, ee = {https://publications.waset.org/pdf/5912}, url = {https://publications.waset.org/vol/72}, bibsource = {https://publications.waset.org/}, issn = {eISSN: 1307-6892}, publisher = {World Academy of Science, Engineering and Technology}, index = {Open Science Index 72, 2012}, }