Using predicate-based model checker for verifying E-Commerce protocols

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 prop- erty specified as a temporal logic formula. Model check- ing 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 defi- nition 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 abil- ity to handle growing amounts of work in a graceful man- ner, 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 prop- erties of E-Commerce protocols. The new predicates are scalable that are used to check gradient properties of dif- ferent 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.