Using Predicate-based Model Checker for Verifying E-Commerce Protocols
Tarek M. I. El-Sakka, M. Zaki · International journal of network security · 2014
Over the past decade, researchers have demonstrated that the technique of model checking can be extremely effective when applied to security or e-commerce protocols. Model checking is the process of determining whether a formal model of the analyzed system satisfies a correctness property specified as a temporal logic formula. Model checking result is either a claim that the property is true or else a counterexample showing that the property is false. E-Commerce protocols are techniques used to secure E-Commerce transactions. E-Commerce protocols have to own one or more from the security properties like safety, aliveness, authentication, and integrity. Unfortunately, the conventional model checking does not have the definition of these security properties, which are essential for the E-Commerce protocols. In addition, scalability is a desirable property of a protocol, which indicates its ability to handle growing amounts of work in a graceful manner, or to be readily enlarged. In this paper, we extend the conventional NuSMV model checker by adding new predicate layers to enhance its ability for verifying properties of E-Commerce protocols. The new predicates are scalable that are used to check gradient properties of different E-Commerce protocols. The new model combines features for model checking with predicate facilities. The new model can analysis and verify E-Commerce protocols easily and effectively. Therefore, we use to analyze some E-Commerce protocols to verify its security properties.