PPF: A model-based tool for analyzing E-payment protocols
Abdalla Shoeb, Sameh Neji, M. Zaki · 2016
E-payment systems by their nature are complex. Thus, with lack of well-designed formal models to provide a suitable method for their modelling and monitoring many challenging tasks will remain unsolvable. The present work aims at designing and implementing an e-Payment Protocols Formalism, PPF, to allow properties examination and verification for e-payment protocols. The proposed formalism was built on a well-established foundation, CSP (Communicating Sequential Processes) for modelling e-payment protocols as it is a concurrent language and includes a variety of operators. After modelling, an on-the-fly refinement algorithm is applied to eventually conclude whether or not the underlying properties are satisfied. Two case studies, Fair Exchange protocol and NetBill protocol, are analyzed by PPF to examine their correctness. PPF produces all traces that causing property failure because it is more beneficial in the analysis phase than producing the first trace only. PPF found some new failure traces in the case studies of the underlying e-payment protocols.