【作者】 边培泉；

【导师】 洪毅； 冯涛；

【作者基本信息】 兰州理工大学 ， 通信与信息系统， 2004， 硕士

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

【Abstract】 Currently, electronic commerce is the heat point of the research and development in each country, Popularization and acceptance of electronic commerce mainly depends on solution of the following properties: security, atomic, privacy and anonymity. Electronic commerce protocol is the comprising framework of electronic commerce, and its security is the key factor to decide the development of electronic commerce. Formal description and analysis are an efficient way to describe electronic commerce protocol and verify their properties. The research in electronic commerce protocols and their security is helpful for designing safe electronic commerce protocols and promoting the development of electronic commerce.Modal logic, as one of formal methods, is perhaps the best known and most influential method, which consists of various statements about belief in or knowledge about messages in a distributed system, as well as inference rules for deriving new beliefs from available belief and /or new knowledge from available knowledge and beliefs. The former corresponds to logic belief, while the latter logic of logic knowledge is useful in analyzing the properties of protocols. BAN is one of logics that got a big frame for its success in analyzing security protocols.In this paper, BAN logic and the extended BAN logic are primarily introduced, and studied in their advantages and weakness. Combing the advantages, we apply a new formal logic language to analyze electronic commerce protocol and their properties. The language has a strong logic and can be applied easily. A famouselectronic micro-payment protocol--NetBill protocol is also simply introduced andabstracted , At last, the abstracted protocol is especially analyzed and verified completely by the new logic.更多还原