关键词: 电子商务协议 不可靠环境 模型检测 原子性 UPPAAL

Abstract:

With the wide application of the Internet, the environment of e-commerce protocols becomes more and more unreliable. We analyse the security of e-comm erce protocols in failure environments using the model checking approach. Our conclusion is that the security properties of an e-commerce protocol may be violated in the presence of site or communication failures. We evaluate which failures cause the violation of one or more of the properties according   to the message sequence which is produced by the model checking tool UPPAAL. The amended protocol retains the security properties.

Key words: （e-commerce protocol, failure environment, model checking, atomicity, UPPAAL）