#TITLE_ALTERNATIVE# - HALIM ALFATH PRAMONO (NIM 13203140), MUHAMMAD
On the previous research written by Mirza Azhari [11], several Mobile Payment Protocols have been designed. These protocols have proven Atomicity, Effectiveness, and Non-Repudiation Claims. But these protocols did not consider network factor in its process. In this final project, the effects of network factors (delay and message lost) on previous protocol [11] are analyzed. Then protocols that consider network factor are developed. The new protocols that have been developed by concerning network factors are then simulated and verificated by using SPIN model checker program. To run the model protocol in the SPIN program, the model protocol have to be written in PROMELA language. After that the simulations result from SPIN are then compared with the protocol design. The next step is to verificate correctness and claim transaction properties with the SPIN verification tools. As the result the new developed protocols are proven to be Atomic and Non repudiate.