电子商务协议是保障电子商务安全的一种重要手段。非否认性和公平性是电子商务协议的重要性质，但相对于认证协议和密钥分配协议的保密性和认证性，电子商务协议及其非否认性和公平性的形式化研究还不够充分。 论文对串空间模型的丛理论、诚实理论和认证测试理论进行深入的研究，并在此基础上探讨了将串空间模型应用于电子商务协议安全性形式化分析的方法。为了能反映电子商务协议中加密、签名、完整性保护等多种安全机制，扩展了密码原语，以满足分析复杂安全协议的需要。根据电子商务协议主体利益目标不一致、攻击主要来自内部的特点，扩展了攻击模型，对主体处理消息的能力进行了形式化的定义。为了解决电子商务协议中协议主体动态确定，协议执行路径不唯一确定的问题，扩展了串空间中结点间的因果依赖关系，来描述协议随着协议步骤的不断执行而使协议执行结果发生改变的内在逻辑关联。 论文应用扩展的串空间模型对安全电子支付协议SET的安全性进行了较为全面的分析，首次应用形式化的分析方法对SET的保密性、认证性及完整性进行了严格的论证。同时由于SET协议无法满足交易公平性的缺陷，提出了SET协议的一个改进版本，该版本能满足数字商品交易的公平性。