该论文的主要工作内容包括如下:1.建立密码协议的新的安全模型;将密码协议与协议中用到的密码算法视为一个系统(称为密码协议系统),研究并建立密码协议系统的新的细粒度的安全模型,包括协议部件的结构、密码算法部件(包括:序列密码、分组密码、公钥密码、散列函数等)的结构、以及密码协议部件与密码算法部件二者相结合在一起的结构模型.2.提出适合于新的安全模型的组合分析技术;基于假设/保证的组合推理技术,提出新的假设/保证推理规则,并证明该规则的完备性;设计假设/保证推理算法,以此实现密码协议系统的模型检测;并重点解决系统分解问题、假设函数的设定问题、进程与逻辑相结合的系统特性描述问题、密码协议分析的界的问题等难题.3.研究密码协议的多层安全需求模型;将密码协议的安全需求分为基层需求(包括认证性和好的密钥特性,如:协议的可行性、认证的一致性和时序性、密钥的保密性、新鲜性、专有性、抗泄露性、密钥分配的一致性和时序性等)、中层需求(包括消息的连接性、可区分性、协议运行的匹配性、密钥认证性、抗拒绝服务性等)和高层需求(包括原子性、公平性、完整性、匿名性、不可否认性、可追究性等)多个层次.4.提出密码协议的形式化安全需求逻辑;基于近世代数和时序逻辑,提出密码协议的一种形式化安全需求逻辑(SRL),并着重研究该逻辑的较完善的数学描述和严谨的理论证明,证明该逻辑的正确性与完备性.采用SRL统一地、形式化地描述密码协议的多层安全需求,使密码协议中的多种安全需求能在统一的框架下进行描述和验证,同时,也为密码协议的安全模型构造形式化的安全需求集.并说明该安全需求逻辑具有可扩展性和对不同类型密码协议的普适性.5.构造一个实用的密码协议的模型推理验证系统;扩充密码协议的安全需求逻辑(SRL),设计密码协议的一种形式化描述语言(FSL),把密码协议的形式化描述与安全需求描述统一在SRL之中.同时,把密码协议的形式化分析方法与人工智能技术相结合,设计知识库、有限状态推理机,基于SRL建立一个实用的密码协议的模型推理验证系统(MRV),从工程上实现基于SRL的密码协议的模型检测.并着重阐述MRV系统的总体结构和工作原理,阐述其于SRL逻辑规则的推理流程和协议安全需求的验证方法.以实例说明形式化需求与形式化分析二者可以相互促进.6.研究模型检测与Strand Spaces的结合;研究Strand Spaces中入侵者的strands及κ理想(ideal)的概念,扩充入侵者strands和κ理想中的密码运算类型,在此基础上,研究、设计一种构造协议的κ理想的算法并以此约束入侵者的能力;然而研究、证明对于有效的攻击所需的协议并行运行次数,为模型检测构造一个合理的小系统,解决模型检测中普遍存在的密码协议分析的界(bound)的问题.7.给出实例说明该新的安全模型及形式化分析方法的有效性;运用该文提出的密码协议的安全模型及形式化分析方法对一些密码协议(如Kerberos协议、Denning-Sacco协议、Yahalom协议)进行形式化描述和分析,说明该新的安全模型及形式化分析方法的可行性和有效性.