包邮网络安全协议的形式化分析与验证

前言第1章 绪论1.1 安全协议概述1.1.1 安全协议的基本概念1.1.2 安全协议的缺陷分析1.1.3 安全协议的攻击手段1.1.4 安全协议形式化方法的必要性1.2 形式化技术基础1.2.1 模态逻辑技术1.2.2 模型检测技术1.2.3 定理证明技术1.3 形式化方法在安全协议验证中的应用1.3.1 安全协议形式化理论发展现状1.3.2 安全协议形式化方法发展趋势1.4 本章 小结1.5 习题第2章 基于模态逻辑技术的安全协议分析方法2.1 BAN逻辑2.1.1 基本术语2.1.2 推理规则2.1.3 应用实例2.2 类BAN逻辑2.2.1 GNY逻辑2.2.2 AT逻辑2.2.3 SVO逻辑2.2.4 Kailar逻辑2.3 Bieber逻辑2.3.1 历史模型2.3.2 KT5逻辑2.3.3 CKT5通信逻辑2.3.4 消息的解释2.3.5 认证与保密2.4 非单调逻辑2.4.1 安全协议的Nonmonotomic逻辑描述2.4.2 安全协议的Nonmonotomic逻辑分析2.5 本章 小结2.6 习题第3章 基于模型检测技术的安全协议分析方法3.1 Dolev Yao模型3.2 通信进程方法3.2.1 CSP的基本概念3.2.2 CSP的网络模型3.2.3 协议安全性质的CSP描述3.2.4 CSP协议分析3.3 NRL协议分析器3.3.1 协议描述3.3.2 协议分析3.3.3 实例3.4 模型检测工具Mur3.4.1 Mur系统3.4.2 Mur协议分析过程3.4.3 Mur协议分析实例3.5 模型检测工具ASTRAL3.6 协议分析工具BRUTUS3.6.1 BRUTUS协议描述模型3.6.2 BRUTUS协议属性逻辑3.6.3 BRUTUS协议验证算法3.6.4.BRUTUS协议分析实例3.7 本章 小结3.8 习题第4章 基于定理证明的安全协议分析方法4.1 Paulson归纳法4.1.1 Paulson归纳法简介4.1.2 Paulson归纳法的自动化理论4.1.3 Paulson归纳法协议分析示例4.2 Schneider阶函数4.2.1 阶函数的定义4.2.2 阶函数定理4.2.3 协议分析实例4.2.4 基于阶函数的自动化验证技术4.3 串空间4.3.1 基本概念4.3.2 协议入侵者描述4.3.3 安全属性的表示4.3.4 协议分析举例4.3.5 认证测试方法4.4 重写逼近法4.4.1 预备知识4.4.2 逼近技术4.4.3 对NS公钥协议的描述与分析4.5 不变式产生技术4.5.1 基本概念4.5.2 描述攻击者不可知项集合的不变式4.5.3 描述攻击者可知项集合的不变式4.6 本章 小结4.7 习题第5章 安全协议的形式化设计方法5.1 合成协议模型及其安全性5.1.1 HT模型5.1.2 协议的组合5.2 Fail-Stop协议5.2.1 Fail-Stop协议及其分析5.2.2 复杂协议5.3 BSW简单逻辑5.3.1 模型5.3.2 逻辑5.4 本章 小结5.5 习题第6章 Internet密钥交换协议及其分析6.1 Internet密钥交换协议概述6.1.1 阶段1主模式交换6.1.2 阶段1野蛮模式交换6.1.3 阶段2快速模式交换6.2 IKE三协议的形式化分析6.2.1 采用NRL协议分析器进行形式化分析6.2.2 利用扩展BSW逻辑分析6.3 IKEV2协议概述6.3.1 IKEV2密钥交换6.3.2 密钥算法协商6.3.3 加密密钥与认证密钥6.4 IKEV2协议的形式化分析6.4.1 扩展串空间理论6.4.2 IKEV2协议分析6.5 本章 小结6.6 习题第7章 电子商务安全协议及其分析7.1 早期的电子商务安全协议7.1.1 Digicash协议7.1.2 First Virtual协议7.1.3 Netbill协议7.2 SSL协议及其分析7.2.1 SSL协议介绍7.2.2 SSL协议的形式化分析7.3 SET协议及其分析7.3.1 SET协议的流程7.3.2 双重签名技术7.3.3 数字信封v7.3.4 SEL协议的形式化分析7.4 本章 小结7.5 习题第8章 移动通信安全协议及其分析8.1 移动通信安全协议8.1.1 第1代移动通信安全协议8.1.2 第2代移动通信安全协议8.1.3 第3代移动通信安全协议8.2 AUTLOG认证逻辑对AKA协议的分析8.2.1 AUTLOG认证逻辑8.2.2 协议的形式化描述8.2.3 假设前提8.2.4 协议目标8.2.5 形式化证明8.3 利用认证测试方法对3GPP-AKA，协议进行安全性分析8.3.1 移动用户与移动核心网之间的安全性验证8.3.2 服务网络基站与移动核心网之间的安全性验证8.3.3 服务网络基站与移动用户之间的安全性验证8.4 本章 小结8.5 习题第9章 群组通信安全协议及其分析9.1 群组通信概述9.2 群组密钥管理协议9.3 密钥管理方案9.3.1 集中式密钥管理方案9.3.2 分布式密钥分发方案9.3.3 分担式密钥协商方案9.4 群组密钥交换协议的形式化描述及安全性分析9.4.1 AT-GDH协议9.4.2 AT-GDH2协议9.4.3 AT-GDH3协议9.5 本章 小结9.6 习题参考文献出版说明