Modeling and Verification for the Micropayment Protocol Netpay

Authors: Kaylash Chaudhary, Ansgar Fehnker

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.

Keywords: Model, Verification, Micropayment.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1061924

References:

[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.