电子商务是当前各国研究发展的热点，电子商务的普及与接受取决于以下属性的解决：安全、原子、隐私与匿名，它以电子商务协议为构成框架，而电子商务协议是决定电子商务发展的关键因素，形式化描述和分析电子商务协议并验证它们的属性的有效方法。研究电子商务协议及其安全性，对于我们设计安全的电子商务协议和促进电子商务协议的发展很有帮助。 作为形式化分析方法的一种，逻辑分析方法是迄今为止使用最为广泛的一种方法。就是在安全协议的形式化分析中运用模态逻辑，这一点类似于分布式系统中对知识和信仰演变的分析中的逻辑。此逻辑是由许多不同的声明和参考规则组成的，其中声明是关于分布式系统消息的一些信仰或知识的，而参考规则是由从其它信仰到新信仰或从旧知识及信仰到新知识中导出的，前者符合信仰逻辑，而后者是相应的知识逻辑。信仰逻辑局限于协议验证属性的分析上。其中BAN逻辑在分析安全协议中获得了巨大的成功。 在本文中，作者主要研究了BAN逻辑和其相关扩展逻辑及其缺陷，并说明其分析协议的方法、步骤，研究了它的分析协议的优势和缺陷，然后结合它们的扩展逻辑，引用了一种新的分析电子商务协议属性的形式化逻辑语言，该语言逻辑性强、应用简易，作者还简单介绍了一种小金额的交易协议——NetBill协议，并对其有入侵者的情况下的属性进行了逻辑抽象，最后用作者提出的逻辑对抽象化的NetBill协议属性进行了完全的分析与验证，证实了逻辑是有效和成功的。