在电子商务领域中，安全性问题是个极其敏感而重要的问题，是电子商务能否健康发展的关键。SET(Secure Electronic Transaction)电子商务协议是1996年由MasterCard(维萨)与Visa(万事达)两大国际信用卡公司联合制订的安全电子交易规范。它提供了消费者、商家和银行之间的认证，确保交易的保密性、可靠性和不可否认性，保证在开放网络环境下使用信用卡进行在线购物的安全，已经获得了广泛的应用，并由此产生了巨大的经济效益和社会效益。但由于协议的安全性问题十分微妙，一些本身并不复杂的协议的安全漏洞却在协议使用了相当长的时间后才被发现，因此，对协议进行分析。寻找协议的安全性隐患或证明协议是安全的，对协议的进一步应用和发展都是极其有益的。 本文主要的研究目的是采用模型检测工具SMV对SET安全支付协议进行验证。在以Lu & Smolka对SET协议支付过程的简化模型为研究对象的情况下，建立其形式化模型和有限状态机模型，以及协议安全属性的CTL公式，并在网络环境被入侵者控制的假设下，基于SMV符号模型检测工具对协议进行了分析。结果表明，以Lu & Smolka对SET协议支付过程的简化模型的检测发现两个攻击，令入侵者可通过借记到客户的帐上而购得商品。主要的关键技术和我们所做的工作如下： ● 研究验证安全协议的方法 (1)非形式化法。 (2)形式化法。 ● 研究模型检测 (1)模型检测技术分析协议的方法。 (2)模型检测工具，确定了使用SMV作为工具对安全协议进行模型检测。 ● 介绍了符号化模型检测工具SMV (1)SMV的工作机制。 (2)SMV语言的语法定义等。 ● SET协议及其支付过程分析 (1)SET协议所要达到的主要目标，工作原理，加密技术，参与者等。 (2)SET协议的支付过程主要包括购买请求，支付授权，支付获得三个子协议，对这三个子协议的执行流程及其步骤进行了详细的分析。 ● 运用SMV对SET协议支付过程的模型检测 (1)建立支付过程的抽象模型。 (2)建立协议主体的有限状态转换图。 (3)基于CTL的安全属性描述。 (4)协议安全属性的验证。