随着电子商务在全球的迅猛发展，电子商务的安全问题日益受到人们的关注。安全的电子商务协议是确保电子商务活动可靠开展的基础，而安全协议的形式化分析逻辑则是检验协议是否安全的有力工具。 　　本文首先介绍了电子商务协议的多层安全需求模型，以及安全电子商务协议中涉及的关键基础技术。在此基础之上，本文以最典型的BAN逻辑和Kailar逻辑为例，对已有的形式化逻辑工具进行了深入的分析，以具体的协议分析实例说明了它们存在的不足和缺陷，并针对这些不足和缺陷提出了一种新的形式化逻辑工具。新工具通过对分析步骤的规范和改进，在一定程度上避免了由于不恰当的假设、不合理的理想化等原因导致的错误分析；通过引入了“协议的本次执行”这一概念，能够有效地分析出BAN逻辑所无能为力的重放攻击；通过对“可追究法则”的改进和扩充，克服了Kailar逻辑无法分析签名密文的缺陷；通过增加“密钥判断法则”，能够形式化地证明密钥的性能，有效地弥补了BAN逻辑在这方面的缺陷。新的逻辑工具可以分析协议主体间的信任关系和可追究关系，可用于分析电子商务协议、认证协议以及密钥分配协议等。本文最后通过一系列具体的安全协议分析实例，验证了新工具的性能。