SET协议支付过程的符号模型检验

电子商务协议的安全性是电子商务健康发展的关键。随着SET协议应用的日益广泛,其安全性受到了业界的极大关注。分析、寻找SET协议安全隐患或证明其安全性,将有助于协议的进一步应用和发展。将模型检测应用于分析SET协议,给出SET协议支付过程的形式化模型和有限状态机模型,以及协议安全属性的CTL公式,并在网络环境被入侵者控制的假设下,基于SMV符号模型检测工具对协议进行了分析。结果表明,SET协议拥有保密性、完整性、认证性等电子商务安全需求属性。

Symbolic Model Checking the SET Protocol

The security of electronic commerce protocols is pivotal to the development of electronic commerce. With the widely use of SET, the security of the protocol has got a broad concern in the field. To analyze SET thoroughly, finding out the flaws or verifying the security, will do benefit for the protocol's further application and development. This paper analyzes the SET protocol with model checking method. A formal model and a finite state machine model of the SET payment system, as well as CTL formulations of the security properties are presented. Under the assumption of the networking environment being controlled by the intruder, the protocol is analyzed by SMV model checking tool. The results show that the security requirement properties of the confidentiality, integrity and authentication are hold by the SET protocol. In addition, some relative works about the paper are compared.