Additional service security of e-commerce in mine enterprises

With the e-commerce developing, some mine enterprises established its own websites in order to provide network services. Now, these enterprises have to provide more services for the competition of e-business. The extend services as annexes are proposed. When the additional service added the original protocols of the e-commerce service changed. Because these actions may lead to some security hole the additional services should be checked. How to hold the security of e-business protocols is in front of us. We solve this problem by model checker (NuSMV) which can verify the security property. We analyze the additional service and show how to verify the additional services by model checker. This method can reduce the state spaces of the new service compounded by the original service and the extend one, and also provides a good way to check faults in the joint between the annex and the origin one.