随着电子商务在全球范围的广泛应用,电子商务的纠纷也越来越多。在众多的电子商务纠纷中,相当一部分是由于电子支付协议本身的缺陷引起的。因而电子支付协议成了电子商务发展的瓶颈。而电子支付协议的原子性是用来规范电子交易活动中的资金流、信息流、和物流,因而是导致支付过程中产生纠纷的重要原因之一。因而,近年来,电子商务协议的原子性成了研究的热点。人们针对电子支付协议的原子性提出了诸多的协议,企图解决这个问题。电子商务协议的设计是一个十分庞大和复杂的工作,而且极易出现意想不到的错误,一个看是完美无缺的协议可能存在各种漏洞。这样电子商务协议的原子性的分析验证就成了一个现实的课题。 目前对电子商务协议的检验手段主要有:直观的分析,实际攻击测试和形式化的检验分析技术。由于形式化分析借助于形式化分析方法和工具完成,具有逻辑严密和断言普遍的优点,但是形式化分析中的逻辑验证需要初始假设的非形式化过程,以及对协议进行理想化等缺陷。Gavin Lowe首先使用CSP和模型检验技术对密码协议进行分析,它克服了逻辑验证的上述缺陷。模型检验在电子商务协议安全性分析验证方面得到了广泛的应用。 本文应用符号模型检验器(SMV)对电子商务协议的原子性进行分析,在对SET协议进行形式化描述的基础上,对SET协议进行分析和检验,指出了协议的缺陷。同时对该协议进行改进,又对改进后的协议的进行分析和检验,表明应用符号模型检验器对电子商务协议分析检验的可行性。