The application of model checking for securing e-commerce transactions

Model checking is an evolving technology for effective and efficient evaluation of e-business protocols. The technology is based on automated techniques such as simulation or theorem proving. E-business managers, developers, and auditors require tools to assure users that e-business systems are secure and reliable. Money atomicity, goods atomicity, and validated receipt are critical e-process requirements in addition to designing effective e-business protocols. Model checking provides verification of whether or not our system guarantees these requirements by writing them as specifications in the model checker. The model checker returns a counter example which allows the analyst to immediately see how the requirement can be violated, if a specification is not specified, which helps in modifying the system to resolve the problem. The assurance provided by model checking can ensure greater confidence in e-process and thereby increase the acceptance and legitimacy of e-business.