Modeling and Verification for the Micropayment Protocol Netpay
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.
[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.
[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.
@article{"International Journal of Engineering, Mathematical and Physical Sciences:55002", author = "Kaylash Chaudhary and Ansgar Fehnker", title = "Modeling and Verification for the Micropayment Protocol Netpay", 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.", volume = "6", number = "12", pages = "1661-9", }
