作为电子商务的重要组成部分,基于Internet的电子交易受到了广泛的关注。SET交易过程十分复杂,在完成一次SET协议交易过程中,需验证电子证书9次,验证数字签名6次,传递证书7次,进行签名5次,4次对称加密和非对称加密。由于SET协议在设计阶段过程复杂庞大,通过国内外许多研究表明SET’协议也有许多不足之处,例如:(1)SET协议中没有描述支持不可抵赖,尽管采用了数字签名技术,在一定程度上支持了不可抵赖特性。(2)在SET协议中,银行网关具有很大的权力,可以认可该交易的成功与否。若偏袒任何一方,将损害另一方的权益。但可以采取两个策略改进,其一,支付网关设立电子公告板,公告每次交易的签名散列值,提供质询,客户商家均可查询；其二,增加一个类似公证性质的职能机构,该机构用以备份交易中的双重签名及持卡者和商家的有关信用认证信息。(3)SET协议的凭证证书格式只是要求遵守X.509规范,并没有强调要求各种不同的应用环境兼容。所以我们在建立电子商务平台时,应尽可能考虑证书的兼容性,周密设计其扩展域以易于过渡到不同的交易平台。(4)S ET协议的安全在一定程度上也依赖于外部环境。如HTTP及SMTP两个协议、浏览器与电子邮件的实时性等,SET协议实施时有可能出现许多的问题,要求我们能统筹考虑,尽可能提高系统的安全性。对SET协议的安全性进行分析,寻找其安全隐患或证明其为安全的,对协议的进一步推广、应用和发展具有重要实际意义　　 为充分验证SET协议的交易安全性,发现SET协议在交易过程中的各种缺陷,本文采用了模型检测方法对SET。协议进行分析和验证。SPIN是一种基于LTL(线性时序逻辑)的通用的自动验证工具,输入协议及环境的模型和用LTL表示的正确性要求,如果模型不满足要求,能够给出反例,也即对协议的攻击。在使用SPIN时,要避免状态空间爆炸的问题,主要是攻击者建模要求技巧,这对验证效率和结果都有影响。研究一种普遍性的建模方法很有意义。本文选取SET协议的核心部分:购买请求、支付认证和获得付款三个子协议过程作为研究分析对象,对SET进行SPIN模型检测,并根据分析模拟与验证的结果对SET进行改进。