Modeling and Verification of Contactless Mobile Banking System in E-Banking Using SPIN

During this prevailing generation of the digital world, mobile users are multiplying globally by leaps and bounds. A mobile banking system is an electronic channel for Electronic Banking (E-Banking) all over the world. The utility of mobile banking systems has become one of the innovations to transform financial institutions from the traditional to the digital world with all the banking services. However, financial institutions do not provide enhanced banking services and electronic cheques using the mobile banking system globally. This paper proposes a new contactless mobile banking system (C-MBS) that integrates enhanced banking services with novel functions like electronic cheques, registration of the user, and cancellation of the user account included in the model. This paper develops an extended finite state machine model with parameters, variables, and constraints for C-MBS. This paper also develops a verification model of C-MBS with system properties specified utilizing process meta language (PROMELA) and security properties applying linear temporal logic (LTL). A simple promela interpreter (SPIN) is employed to verify the verification model of C-MBS. SPIN verification results confirm that the proposed C-MBS model is free from deadlocks and errors. Hence, the financial institutions can implement this model as a secure enhanced mobile banking system in E-banking. Banking users can use the enhanced banking services remotely using C-MBS on mobile and will play a significant role towards a cashless society in the digital world.