密码协议形式化分析PDF电子书下载

第1章　引论 1

1.1　密码体制 1

1.1.1　基本原理 1

1.1.2　密码体制分类 1

1.2　数字签名 3

1.2.1　数字签名技术 4

1.2.2　数字签名技术与加密技术的结合 5

1.2.3　几种新型的数字签名方案 5

1.3　Hash函数 7

1.4.1　密钥的管理问题 8

1.4　密钥管理 8

1.4.2　密钥的生成 9

1.4.3　密钥的分配 9

1.5　PKI公钥基础设施 11

1.5.1　PKI的基本组成 11

1.5.2　PKI的安全服务 12

1.5.3　PKI的信任模型 13

1.6　本章小结 13

1.7　习题 13

2.2.1　密码协议的概念 15

2.2　密码协议基本概念 15

2.1 引言 15

第2章　密码协议概述 15

2.2.2　密码协议的分类 17

2.2.3　密码协议的安全性质 18

2.3　密码协议的缺陷及所受到的攻击实例 19

2.3.1　基本协议缺陷 20

2.3.2　口令猜测攻击 20

2.3.3　重放攻击 21

2.3.4　类型攻击 22

2.3.5　并行会话攻击 23

2.3.7　绑定攻击 24

2.3.6　与实现相关的攻击 24

2.3.8　封装攻击 25

2.3.9　其他形式的攻击 25

2.4　密码协议的设计与分析 26

2.4.1　密码协议的设计规范 26

2.4.2　密码协议的安全分析 27

2.5　密码协议形式化分析的研究与进展 27

2.5.1　形式化分析前提 27

2.5.2　形式化分析的历史与现状 28

2.5.3　形式化分析面临的挑战 33

2.5.4　协议形式描述语言进展 35

2.5.5　形式化分析对密码协议设计的贡献 35

2.6　本章小结 35

2.7　习题 36

第3章　形式逻辑方法 38

3.1　BAN逻辑 38

3.1.1　BAN逻辑框架介绍 38

3.1.2　BAN逻辑分析协议举例 40

3.1.3　BAN逻辑的缺陷 45

3.1.4　BAN逻辑的改进 48

3.1.5　认证协议的BAN逻辑设计准则 63

3.2　扩展的BAN逻辑 68

3.2.1　GNY逻辑 68

3.2.2　MB逻辑 72

3.2.3　AT逻辑 75

3.2.4　VO逻辑 81

3.2.5　SVO逻辑 82

3.3　BAN类逻辑现状 86

3.4　Kailar逻辑 86

3.4.1　基本符号 86

3.4.3　推理规则 87

3.4.2　基本语句 87

3.4.4　分析协议举例 88

3.5　本章小节 90

3.6　习题 90

第4章　模型检测方法 91

4.1 引言 91

4.2　模型检测技术分析密码协议的方法和结果 92

4.2.1　模型检测技术分析密码协议的方法研究 92

4.2.2　模型检测的现状及问题 93

4.3.1　CSP协议模型 94

4.3　CSP及FDR模型检测技术 94

4.3.2　入侵者模型 95

4.3.3　协议系统模型 95

4.3.4　协议目标的描述 96

4.3.5　协议目标的验证 97

4.3.6　Casper介绍 97

4.4　Mur？模型检测技术 97

4.4.1　Mur？协议模型 97

4.4.2　入侵者模型 99

4.4.3　协议目标的描述 99

4.5　Brutus模型检测技术 100

4.5.1　Brutus协议模型 100

4.4.5　状态缩减技术 100

4.4.4　协议目标的验证 100

4.5.2　入侵者模型 102

4.5.3　协议目标的描述 102

4.5.4　协议目标的验证 102

4.5.5　状态缩减技术 103

4.6　模型检测工具SMV 103

4.6.1　SMV简介 103

4.6.2　SMV语言 104

4.6.3　一个SMV实例 105

4.6.4　SMV分析举例 107

4.7　本章小节 111

4.8　习题 111

第5章　定理证明方法 112

5.1　定理证明方法介绍 112

5.2　归纳方法 112

5.2.1　归纳方法简介 112

5.2.2　Otway-Rees协议分析 115

5.3　Schneider阶函数 118

5.3.1　事件、进程和迹 118

5.3.2　阶函数的定义 119

5.3.3　阶函数定理 120

5.3.4　实例分析 121

5.3.5　新版阶函数 125

5.4　串空间方法 126

5.4.1　串空间的基本概念 126

5.4.2　入侵者的形式化 130

5.4.3　安全特性的表示 132

5.4.4　一个ISO候选协议分析 133

5.4.5　串空间方法的扩展 135

5.5　重写逼近法 139

5.5.1　预备知识 140

5.5.2　逼近（Approximation）技术 141

5.5.3　对NS公钥协议和攻击者的编码 143

5.5.4　逼近和验证 145

5.6　不变式产生技术 147

5.6.1　基本概念 147

5.6.2　描述攻击者不可知项集合的不变式 148

5.6.3　描述攻击者可知项集合的不变式 150

5.7　本章小节 151

5.8　习题 152

第6章　密码协议的设计准则 153

6.1　密码协议的基本设计准则 153

6.2.2　消息明确性的作用 156

6.2　基本设计准则对于公钥协议的局限性 156

6.2.1　加密与签名的顺序 156

6.3　几条更直观的设计准则 157

6.4　本章小节 158

6.5　习题 158

第7章　密码协议分析主要的形式化语言和分析工具 159

7.1　接口描述语言 159

7.2　通用认证协议描述语言 161

7.3　Casper 163

7.4　自动认证协议分析器 163

7.5 NRL与FDR 165

7.7　本章小结 167

7.6　定理证明器 167

7.8　习题 168

第8章　几个具体密码协议的实现方法和工作原理 169

8.1 Kerberos 169

8.1.1　Kerberos概况 169

8.1.2　票据标志使用与请求 173

8.1.3　消息交换 175

8.1.4　Kerberos的优缺点 180

8.2　IPSec 180

8.2.1　IPSec体系结构 181

8.2.2　IPSec的安全策略 182

8.2.3　IPSec的安全协议 185

8.2.4 1PSec的应用 196

8.3　SSL 196

8.3.1　SSL的工作原理 198

8.3.2　SSL的体系结构 198

8.3.3　SSL的安全性 203

8.4　X.509 206

8.4.1　X.509公钥证书概述 206

8.4.2　证书及其扩展 211

8.4.3　CRL及其扩展 221

8.4.4　证明路径验证 224

8.4.5　算法支持 226

8.5　SET 229

8.5.1　SET协议简介 229

8.5.2　SET协议工作流程 230

8.5.3　SET的认证 232

8.5.4　证书请求协议 233

8.5.5　SET与SSL的比较 242

8.6　本章小结 244

8.7　习题 244

参考文献 246