Commenced in January 2007
Frequency: Monthly
Edition: International
Paper Count: 31231
Modeling and Verification for the Micropayment Protocol Netpay

Authors: Kaylash Chaudhary, Ansgar Fehnker


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.

Keywords: Verification, model, Micropayment

Digital Object Identifier (DOI):

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1065


[1] X. Dai and J. Grundy. Architecture for a component-based, plug-in micro-payment system. In In Proceedings of the Fifth Asia Pacific Web Conference. LNCS, Springer, April.
[2] X. Dai and J. Grundy. Three kinds of e-wallets for a netpay micropayment system. In The Fifth International Conference on Web Information Systems Engineering, pages 66-67, Brisbane, Australia, November 22-24 2004. LNCS 3306.
[3] X. Dai and J. Grundy. Architecture of a micro-payment system for thinclient web applications. In In Proceedings of the 2002 International Conference on Internet Computing. CSREA Press, June 24-27.
[4] S. Glassman, M. Manasse, M. Abadi, P. Gauthier, and P. Sobalvarro. The millicent protocol for inexpensive electronic commerce. In Fourth International World Wide Web Conference, December 1995.
[5] R. Rivest and A. Shamir. Payword and micromint: Two simple micropayment schemes. pages 307-314. LNCS, 1998.
[6] A. Herzberg and H. Yochai. Mini-pay: Charging per click on the web. 1996.
[7] R. Hauser, M. Steiner, and M. Waidner. Micro-payments based on ikp. In Proceedings of 14th Worldwide Congress on Computer and Communications Security Protection, pages 67- 82, Paris-La Defense, France, December 22-24 1996. Lecture Notes in Computer Science.
[8] N. Nisan, S. London, O. Regev, and N. Camiel. Globally distributed computation over the internet. the popcorn project. In 18th International Conference on Distributed Computing Systems (18th ICDCS-98), pages 592-601, Amsterdam, The Netherlands, 1998. IEEE.
[9] N. Lynch and M. Tuttle. An Introduction to Input/Output automata. Technical Memo MIT/LCS/TM-373, Massachusetts Institute of Technology, November 1988.
[10] X. Dai, J. Grundy, and B. Lo. Comparing and contrasting micropayment models for e-commerce systems. In Proceedings of the International Conferences of Info-tech and Info-net (ICII), China, 2001.
[11] Y. Kawabe, K. Mano, H. Sakurada, and Y. Tsukada. Theorem proving anonymity of infinite systems. Information Processing Letters, 101(1):46-51, 2007.