安全协议分析与设计

第1部分 软件工程基础

第1章 引言

1.1 安全协议基础知识

1.2 安全协议形式化分析的现状

1.3 基本概念和协议记法

1.4 协议分析的假设

1.4.1 完善加密假设

1.4.2 单一协议假设

1.4.3 诚实主体假设

1.4.4 随机数和时间戳的假设

1.5 攻击者能力分析

1.5.1 攻击者能力分解

1.5.2 攻击者划分

1.5.3 攻击类型

1.6 密码算法基础知识

1.6.1 密码算法

1.6.2 对称密码算法

1.6.3 hash函数

1.6.4 公开密钥算法

1.6.5 密码算法提供的服务

习题

第2章 安全协议及攻击

2.1 身份认证协议

2.1.1 无可信第三方

2.1.2 有可信第三方

2.2 密钥建立协议

2.3 安全协议的目标

2.3.1 认证目标

2.3.2 密钥建立目标

2.3.3 其他目标

习题

第3章 逻辑类分析方法

3.1 概述

3.1.1 逻辑类分析方法

3.1.2 逻辑类分析方法的特点

3.2 ban逻辑

3.2.1 ban逻辑系统

3.2.2 用ban逻辑分析安全协议

3.2.3 ban逻辑的局限性

3.3 ban类逻辑

3.3.1 gny逻辑

3.3.2 at逻辑

3.3.3 mb逻辑

3.4 svo逻辑

3.4.1 svo逻辑的认证目标

3.4.2 svo逻辑语法

3.4.3 svo逻辑语义

3.4.4 用svo逻辑分析安全协议

习题

第4章 模型检测分析方法

4.1 概述

4.1.1 通用的形式化验证方法

4.1.2 专用的形式化检验系统

4.2 csp方法

4.2.1 基本术语和示例

4.2.2 协议目标的描述

4.3 分析实例

4.3.1 用csp验证nspk协议

4.3.2 用csp验证tmn协议

习题

第5章 定理证明类分析方法

5.1 概述

5.1.1 paulson归纳法

5.1.2 schneider秩函数

5.1.3 串空间证明方法

5.1.4 复杂性证明理论

5.2 串空间证明方法

5.2.1 串空间理论

5.2.2 串空间证明过程

5.3 定理证明分析的局限性

习题

第6章 安全协议的设计

6.1 安全协议设计的基本原则

6.1.1 基本原则

6.1.2 命名原则

6.1.3 加密原则

6.1.4 时间性原则

6.1.5 识别原则

6.1.6 信任原则

6.2 安全协议的设计方法研究

6.2.1 安全协议设计方法概述

6.2.2 fail-stop协议

6.2.3 ck模型

6.3 设计抵御拒绝服务攻击的安全协议

6.3.1 安全协议中的dos攻击

6.3.2 无状态连接方法

6.3.3 cookie方法

6.3.4 failing-together方法

6.3.5 clientpuzzle方法

习题

第7章 实用安全协议

7.1 kerberos网络认证服务

7.1.1 概述

7.1.2 报文交换

7.1.3 协议特点

7.2 x.5 09标准

7.2.1 概述

7.2.2 证书

7.2.3 认证协议

7.2.4 协议特点

7.3 传输层安全协议

7.3.1 概述

7.3.2 会话和连接

7.3.3 握手协议

7.3.4 tls协议的简化描述

7.3.5 协议特点

7.4 internet密钥交换协议

7.4.1 概述

7.4.2 ipsec与isakmp

7.4.3 使用数字签名认证的ike第一阶段

7.4.4 使用公钥加密认证的ike第一阶段

7.4.5 使用修订的公钥加密认证的ike第一阶段

7.4.6 使用预共享密钥认证的ike第一阶段

7.4.7 ike第二阶段——快速模式

7.4.8 新组模式

7.4.9 协议特点

7.5 ppp认证与radius

7.5.1 radius

7.5.2 pap和chap

7.5.3 扩展认证协议

7.6 无线局域网的认证与密钥管理

7.6.1 wep的加密及认证

7.6.2 802.1 1i与802.1

7.6.3 wpa与tkip

7.6.4 wpa的密钥管理

7.7 gsm认证

7.7.1 gsm系统概述

7.7.2 gsm用户认证及密钥建立

7.7.3 协议特点

7.8 3g安全协议

7.8.1 wcdma与cdma2000简介

7.8.2 wcdma接入安全

7.8.3 cdma2000接入安全

附录A 协议及攻击索引

参考文献

《安全协议分析与设计》系统地介绍了安全协议（主要是认证协议和密钥建立协议）的基本概念、攻击方法、分析方法和设计方法。全书分为7章，从安全协议的基本概念和协议记法出发，先介绍安全协议分析采用的假设和对攻击者能力的界定，接着对一些经典的安全协议及其攻击展开分析，然后对逻辑类分析方法、模型检测分析方法和定理证明类分析方法分别进行介绍，并讲述了安全协议的设计原则和设计方法，最后对一些实际使用中的具体安全协议进行讲解和分析。《安全协议分析与设计》注重知识的系统性和覆盖面的广泛性，部分内容有一定的理论深度。
《安全协议分析与设计》可作为信息安全、计算机、通信专业的本科生和研究生教材，也可作为相关专业的研究人员和工程技术人员的参考书。

《安全协议分析与设计》使用通俗易懂的语言，力图使一个没有信息安全基础的初学者，在较短时间内，可以较为容易地掌握安全协议相关的基本理论和方法；在章节安排上由浅入深，在读者对协议和攻击有了初步的认识之后，才开始介绍难度较大的理论分析方法和设计方法；《安全协议分析与设计》注重逻辑性和实践性，在通读之后，会对安全协议有一个较为全面的把握，并可具备初步的协议分析能力和设计能力。
透彻易懂的概念诠释，深入浅出的协议分析和讲解，涵盖大量常见安全协议的分析和设计。