由于互联网的普及,随之而兴起的电子商务已经成为一个新的商业交易模式,而相应的电子商务协议则是这一新型的交易模式顺利进行的保证。网络环境下协议的安全、原子、隐私与匿名这些属性的有效解决则是电子商务广泛应用关键。而严格的形式化描述和分析是刻画电子商务协议并验证它们相应属性的有效方法.电子商务协议作为安全协议当中的一类重要协议,除了具有一般的安全协议所应当具备的性质以外,还有其一些专有的独特性质。本文首先介绍了安全协议形式化分析的研究现状和主要方法,并且重点讨论了其中的模型检测方法。还对电子商务协议的研究状况做了简要介绍。概括了电子商务协议的分类并且对原子性、不可否认性、公平性等主要的安全性质归纳讨论。最后以一个具体的电子商务协议为例,使用CSP为建模语言刻画了该协议和并以电子商务协议中公平性作为需要验证的属性,以基于CSP的FDR为相应的模型验证工具,用有限自动机结构对模型所有状态集合进行检验,检测该协议是否特定的一些公平性(即金钱原子性,货币原子性和有效接受性),并且在模型中引入网络环境下很容易出现的两大故障(即断线和网站故障),观察引入故障后相应的性质能否保持并分析其原因。并且提出一些可能的修改意见对协议加以完善。