密码协议的安全性研究是网络安全研究的主要热点。本论文主要研究了如何应用系统工程思想和形式化方法来分析和设计密码协议,取得的主要研究结果如下:1.将系统工程思想引入密码协议设计,结合前人的研究成果,提出了10条密码协议工程原则:5条安全需求分析原则,4条详细设计原则以及1条安全性证明原则。将密码协议设计看作密码协议工程,从协议设计的不同阶段给出原则,是帮助研究人员按系统工程思想进行密码协议设计的有益尝试。实例分析表明,这些原则不仅较为完备,而且可操作性强,能帮助研究人员明确协议设计背后的隐含假设,发现和避免协议设计中的漏洞,简化协议设计。2.首次提出基于信任的新鲜性标识符分析密码协议的安全性,给出了新鲜性原则:对每个通信参与主体而言,密码协议的安全性取决于发送或者接收的、包含自身已相信新鲜的新鲜性标识符的单向变换。该原则找到了一条快捷、有效的密码协议安全性分析方法,论文示例了20多个经典密码协议的分析结果,分析出的针对协议的攻击或者安全隐患有12个是以往没有指出过的。新鲜性原则的特点是:①能有效区分消息是否新鲜,安全性的分析独立于并发运行环境的具体形式化描述,也独立于攻击者能力的具体形式化描述;②基于该原则得到的分析结果能够证明正确协议的安全性,也能够分析出不安全协议存在的安全属性缺失,以及由该缺失直接构造攻击的结构。3.基于新鲜性原则,提出了基于逻辑推理的信任多集形式化分析方法。以Needham-Schroeder公钥认证协议为例,说明了该分析方法的有效性、严谨性和自动化实现的可能。另外,针对无线网络的开放性和数据包易失的特点,扩展了信任多集方法,能有效用于无线密码协议分析。4.证明了保证认证协议安全的充分必要条件,这些条件在计算模型下分别满足基于匹配对话和不可区分性的4个可证安全定义。5.提出了信任多集自动分析工具的总体框架,通过在2种不同开发环境下信任多集自动分析工具初步实现的比较,给出了信任多集自动分析工具的详细设计。正在开发的信任多集自动分析工具已成功实现了对若干密码协议的安全性分析。6.基于新鲜性原则和因果一致性的分布式逻辑时间,建立了信任多集形式化设计方法。构造了一个公钥认证协议,并证明了该协议达到了消息数和轮数的下限。