EXTENDED NUSMV MODEL CHECKER

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. One of the most successful symbolic model checkers is the branching time model checker SMV (Symbolic Model Verifier). NuSMV originated from the reengineering, reimpIementation and extension of SMV. E-Commerce protocols are techniques used to secure E-Commerce transactions. E-Commerce protocols have to own one or more of the security properties like safety, aliveness, authentication, and integrity. Unfortunately, the conventional NuSMV model checker does not have the definition of these security properties, which are essential for the E-Commerce protocols. In this paper, we propose an extension to the conventional NuSMV model checker by adding new predicate layers to enhance its ability for verifying properties of E-Commerce protocols. We develop general predicates to represent the security properties of E-Commerce protocols. The new model combines features for model checking with predicate facilities. We use the new extended model to analyze some E-Commerce protocols to verify its security properties