计算机网络的出现使世界的联系变得更加紧密。但是，开放式网络上和分布式系统上不断增长的各种应用尤其是电子商务的蓬勃发展，对系统的安全提出了巨大挑战，不能有效地解决计算机网络信息的安全问题，就会影响到计算机网络应用更广，更高，更深的发展。构造安全的计算机系统是一个复杂的体系，其中身份认证系统作为系统安全，网络安全的第一道防线，对整个系统的安全具有非常重要的作用。实现身份认证的方式有很多种，其中最安全的方式是基于密码技术的身份认证协议，但一个好的密码算法并不能保证协议的安全，许多认证协议在公布后被发现有漏洞，因此，如何保证认证协议的安全就成为研究人员的重要任务，在本文中我们研究的不是认证协议的密码算法，而是对协议本身结构的分析，我们采用形式化的逻辑方法来衡量一个认证协议的好坏，分析协议是否安全、高效等等。电子商务迅速发展产生的各种需求需要安全可靠公平合理的交易协议，电子商务安全的核心就是要解决交易主体之间相互信任的问题。电子商务是一种网络交易系统，用以实现电子货币的支付和服务的兑现，本身通过协议来实现。电子商务协议的设计必须满足可追究性原则，即参与交易的双方不能对自己的发出的信息进行否认，但是，电子商务协议是否遵循可追究性原则不仅依赖于所采用的密码算法的安全强度, 依然与协议的自身结构有着密切的联系。在交易中我们不仅要满足主体对所分配的密钥的信任要求，更关键的是提出服务要求的主体要确信自己能得到所需要的服务，提供服务的主体也要确信自己能收到应得的电子货币，而作为两者中间的货币中介机构要能向双方提供证明和担保，并实施电子货币的支付。形式化的逻辑方法经过改进依然在分析电子商务协议中发挥重要作用。本文主要是对形式化逻辑方法在分析基于密码技术的认证协议和电子商务协议中的应用作了一些研究。其主要工作如下：1.对形式化分析方法的研究状况作了介绍，指出形式化分析方法能全面的，深刻的分析认证协议和电子商务协议中的设计漏洞。2.根据BAN逻辑对Needham-Schroeder公钥分配认证协议的分析结果，基于协议理想化规则和设计指导原则，本文对Needham-Schroeder公钥分配认证协议作了改进，设计了一个建立在对称密码体制上的认证协议的基本模型，并使用BAN逻辑给予了正确性证明。3.在认证协议中，入侵者在多数情况下是利用协议中的参与主体名称，新的会<WP=57>话密钥，新鲜性标识三者之间的关联关系的漏洞以及协议中出现的结构一致的消息而进行攻击的。本文总结了几条新的指导性设计原则来帮助协议分析者发现协议的漏洞，进而提出改进方法；协议设计者可以遵循这些原则来设计协议，避免一些已被发现的协议错误。4.鉴于Kailar逻辑缺乏对电子商务协议公平性分析功能的缺陷，扩展了其逻辑推理框架，将协议参与主体的局部状态定义成一个三元组，即主体当前相信的公式集合，主体曾看到的公式集合，主体拥有的密钥集合；并提出了几条新的推理规则；此方法可以用来分析电子商务协议的安全性，可追认性以及公平性等属性原则。本文用这种扩展逻辑对Bolignano电子支付协议公平性作了分析，并给出改进办法。5.由于逻辑推理所涉及的大多是符号和规则, 此推理过程若要由人工来完成, 则无论在人力上, 还是在时间上均会造成极大的浪费, 根据逻辑推理容易在计算机上实现的特点, 我编写了基于这个逻辑框架的Prolog 的协议验证系统, 用来验证一些认证协议和电子商务协议，对认证协议的验证目标是一级信仰以及二级信仰，对于电子商务协议而言，则分析验证其可追究性以及公平性。其中协议的初始化过程以及协议转换成逻辑的过程由验证者来完成，推理部分则由系统来进行，来达到验证协议是否符合所要达到的目标的目的。6.不可否认性作为电子商务最基本的要求，必须提供不可否认证据的产生、收集和维护机制以防止交易的任何一方试图对交易中已发生的特定事件或行为的否认。另外，公平性也是电子商务协议必须考虑的因素，它保证交易的任何一方在交易中不能通过作弊手段而取得优于另一方的优势地位。 本文根据这两个需求提出了一个公平的，具有不可否认性的电子商务协议 , 并使用扩展的逻辑分析证明了它的不可否认性以及公平性原则。