随着网络通信技术的发展,电子商务已经渗透到人们的日常生活中。电子商务协议的安全性是决定电子商务发展的关键因素之一,也是制约电子商务发展的瓶颈。目前分析电子商务协议安全性的方法主要有BAN逻辑、模型检测和归纳方法等。虽然上述方法都能够较好地分析协议的某些安全属性,但都具有一定的局限性。串空间理论是一种新的分析协议安全性的形式化方法,它充分吸收了前人的研究成果。但是串空间模型最初提出来只限于对认证协议的分析,很少涉及电子商务协议。电子商务协议比认证协议更为复杂,它不仅要满足认证协议的安全需求,还要考虑认证协议中未涉及的若干安全属性,因此有必要找到一种严谨有效的方法来分析电子商务协议的安全性。本文利用串空间理论分析了电子商务协议的安全性,提出了利用串空间模型形式化地描述和验证电子商务协议安全性的思路,设计了一个新的电子支付协议,并验证了该协议的安全性。主要工作包括:(1)在深入研究串空间理论的基础上,提出了利用串空间模型验证电子商务协议安全性的一般性方法,并以著名的电子商务协议—IBS协议为例,通过对其建立串空间模型并引用所提方法对其安全性进行分析,发现该协议的提供服务和传递发票阶段均不满足公平性,得出了与国内外学者用其他形式化方法分析相同的结论,从而验证了串空间模型的有效性和正确性。在此基础上对IBS协议进行了改进,利用串空间理论证明了改进后的协议满足安全性。(2)设计了一个基于同时生效签名的电子支付协议,该协议采用同时生效签名的算法,有利于实现交易的公平性:在交易过程中没有第三方的参与,提高了协议的执行效率,且可用于移动支付。通过对该协议建立串空间模型并进行形式化的分析,可验证其满足秘密性、认证性、公平性、不可否认性及可追究性,因此协议是安全的。(3)基于J2ME平台,利用手机模拟器,开发出上述支付协议的移动客户端。在安全性方面,引用BouncyCastle轻量级加密包,用于客户端移动手持设备对交易信息进行加密运算,保证了端对端的安全性,具有一定的现实意义。