Title: Micropayment proposal with formal verification using coloured Petri nets and performance analysis on the Android platform

Authors: Andreu Pere Isern-Deyà; M. Magdalena Payeras-Capellà; Macià Mut-Puigserver; Josep-Lluis Ferrer-Gomila; Llorenç Huguet-Rotger

Addresses: Universitat de les Illes Balears, Cra. de Valldemossa, km 7.5. Palma de Mallorca, Illes Balears, Spain ' Universitat de les Illes Balears, Cra. de Valldemossa, km 7.5. Palma de Mallorca, Illes Balears, Spain ' Universitat de les Illes Balears, Cra. de Valldemossa, km 7.5. Palma de Mallorca, Illes Balears, Spain ' Universitat de les Illes Balears, Cra. de Valldemossa, km 7.5. Palma de Mallorca, Illes Balears, Spain ' Universitat de les Illes Balears, Cra. de Valldemossa, km 7.5. Palma de Mallorca, Illes Balears, Spain

Abstract: Payments involving small amounts of money are usual in the online purchases of low-value services, goods or pieces of information. In these kinds of payments, called micropayments, a trade-off between efficiency and security requirements has to be provided. In a previous work, we presented an efficient and secure micropayment scheme which fulfils both the security properties that guarantee no financial risks and the desired privacy for customers. In order to prove the viability of the proposal, we have proceeded in two directions. First we have formally verified the protocol using coloured Petri nets (CPN). Secondly, once we are able to assure, from the results of the formal verification, that the proposal satisfies the claimed properties, we have successfully implemented the scheme on the Android platform. Using the developed implementation, we have evaluated its performance to prove that the proposal is viable using current mobile devices. Several tests validate that our scheme can execute very fast payments with our simple but secure spending protocol. With the presented formal verification and performance analysis we can assure that the protocol is ready to be used.

Keywords: micropayment; formal verification; coloured Petri nets; implementation; performance evaluation; Android platform; smartphones; business intelligence; small payments; online payments; security; financial risk; privacy; modelling.

DOI: 10.1504/IJBIDM.2013.055786

International Journal of Business Intelligence and Data Mining, 2013 Vol.8 No.1, pp.74 - 104

Published online: 28 Jun 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article