该文作者经过辛勤研究,在以下几个方面取得了一些成绩,通过实例分析和比较,显示我们方法的可行性和其中某些技术具有一定的领先性:1)发现了密码协议中消息关联特征,并能抽取关联因子作为分析对象.我们对这两个概念进行了形式化的定义,利用CSP分析工具FDR2对Needham-Schroeder公钥协议和Denning-Sacco协议的相关性进行了实例分析发现了有效的攻击,证明了这种方法的可行性.协议相关性的提出为形式化定义和描述协议的安全特征提出了新的思路.2)提出协议认证特征的形式化定义—观测等价,观测等价描述了在开放环境中认证协议的安全目标.同时我们借助Dolev-Yao的协议模型对满足观测等价的主体动作序列的进行搜索,间接地找到了攻击路径.3)发现了Kudo逻辑在时间标记分析中的缺陷,提出了改进的时限逻辑体系用于分析电子商务协议中的时限责任问题;利用我们的新方法发现了Kudo提出的电子投递协议中的错误,并对支持时限责任的改进Netbill协议进行了实例分析,说明如何利用我们的逻辑体系进行实际的协议分析.4)针对当前的拒绝服务的攻击,我们提出如何对密码协议分析防止这类攻击的方法.5)我们设计了一种分布式拍卖协议.6)我们基于观测等价和协议相关特性的分析方法,开发了一个协议分析的专家系统.该系统可与用户交互来调整分析过程中的状态,达到加速有效路径的构造.7)我们实现了一个基于秘密分割和群签名的分布式拍卖系统原型,能完成秘密投标拍卖的基本功能并体现分布式拍卖关于安全性和容错性的6点要求.