WASET
	%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