随着电子商务在全球的迅猛发展，电子商务的安全问题日益受到人们的关注。安全的协议是确保电子商务活动可靠开展的基础，而安全协议的形式化分析则是检验协议是否安全的有力工具。同时，随着电子商务的发展，许多新的加解密算法和签名方案被提出，它们引起了人们对更多安全性质的关注。安全协议所采用的密码体制主要有对称密码体制、公钥密码体制、散列函数和数字签名等。这些密码体制适用于不同的用处。对称密码体制适合用来对大量数据加密，但其密钥传输是个问题；公钥密码体制因为加密速度较慢，一般用来进行身份认证或者密钥分配：散列函数主要是应用于消息的完整性检测，消息的起源认证检测等；数字签名是用来满足电子商务中的各种不同的身份认证。安全协议形式化分析有两种模型：符号方法模型和计算方法模型。其中，符号方法的一种，逻辑推理方法是以BAN类逻辑为主的有效的形式化分析方法。BAN类逻辑中典型的是BAN逻辑、GNY逻辑、AT逻辑、VO逻辑和SVO逻辑。这几种逻辑是通过对BAN逻辑的改进发展而来。其中，SVO逻辑是这种逻辑中比较完善的一个，同时也继承了BAN逻辑的简单性，易于扩展。本文主要是针对BAN类逻辑进行了分析。下面是本文所作的主要工作：1)安全协议主要的性质有保密性，完整性，认证性和不可否认性等。本文指出了BAN类逻辑发展中两个大的缺陷——缺少环境模型以及完整性分析的缺失。BAN类逻辑都假设参与协议的主体都是诚实的，这就否定了攻击者可以通过某些手段成为协议主体的可能性，但在网络世界中，这种假设是不可能完全实现的。因此，需要为BAN类逻辑建立一个适合的环境模型。另外，在BAN类逻辑中，初始假设协议所采用的密码方案是完善的，研究人员普遍认为在此条件下，协议的保密性和完整性同时都得到了保证；但是，由于各种密码体制的安全性质的不同，完整性不能仅通过加解密来保证，尤其是BAN类逻辑还假设了一条消息中的两个密文块分两次到达，这就更不能保证消息的完整性了。2)针对缺少环境模型的缺陷，本文首先以Dolev-Yao模型为基础，对其进行改进，将其构建为BAN类逻辑的环境模型，一是提出在协议分析时，虽然不考虑所采用的具体密码算法，但需要对所采用的密码体制进行分析，以确定协议中消息所具有的初始安全性质：二是提出了比较完善的攻击者行为模型，更加真实地刻画协议所处的环境。3)针对完整性分析缺失的缺陷，本文以SVO逻辑为基础，提出对它的改进，建立了完整性的语义，语法表示以及相应的完整性公理，并改进了消息临时性验证公理。最后，通过对Otway-Rees协议增加完整性的改进，并使用改进的SVO逻辑对它进行分析。