安全协议原理与验证PDF电子书下载

第一部分 基础知识 3

第1章 引言 3

1.1 安全协议的研究背景、基本概念 3

1.1.1 安全协议的研究背景 3

1.1.2 安全协议的基本概念 4

1.2 安全协议的安全性分析 5

1.2.1 秘密性 5

1.2.2 认证性 5

1.2.3 完整性 5

1.2.4 不可否认性 5

1.2.5 公平性 6

1.2.6 原子性 6

1.2.7 匿名性 6

1.3 安全协议的形式化分析技术概述 6

1.3.1 安全协议形式化分析方法概述 6

1.3.2 基于知识与信念的逻辑推理方法 8

1.3.3 基于代数模型的状态检验方法 9

1.3.4 基于不变集的代数定理证明方法 10

1.4 本书的安排 11

第2章 密码学基础 14

2.1 密码学概述 14

2.1.1 密码学的发展过程 14

2.1.2 密码学的基本概念 15

2.2 密码体制 16

2.3 对称密钥密码体制 17

2.3.1 代换密码 17

2.3.2 数据加密标准DES 19

2.3.3 高级数据加密标准AES 27

2.4 公钥密码体制 32

2.4.1 单向陷门函数 33

2.4.2 RSA密码体制 34

2.4.3 MH背包体制 35

2.5 数字签名 37

2.5.1 数字签名的基本概念 37

2.5.2 数字签名方案 38

2.5.3 RSA数字签名 38

2.6 哈希函数 39

2.6.1 哈希函数基本概念 39

2.6.2 几种常用哈希函数介绍 40

2.7 本章小结 45

习题 46

第二部分 安全协议原理 49

第3章 安全协议概述 49

3.1 概述 49

3.2 安全协议分类 50

3.3 安全协议的缺陷 52

3.4 安全协议的威胁模型 53

3.5 针对安全协议的攻击 54

3.5.1 重放攻击 55

3.5.2 中间人攻击 55

3.5.3 并行会话攻击 55

3.5.4 反射攻击 56

3.5.5 交错攻击 57

3.5.6 归因于类型缺陷的攻击 57

3.5.7 归因于姓名遗漏的攻击 58

3.6 安全协议的设计原则 59

3.7 本章小结 60

习题 60

第4章 认证与密钥交换协议 61

4.1 无可信第三方的对称密钥协议 62

4.1.1 ISO one-pass对称密钥单向认证协议 62

4.1.2 ISO two-pass对称密钥单向认证协议 62

4.1.3 ISO two-pass对称密钥双向认证协议 62

4.1.4 ISO three-pass对称密钥双向认证协议 62

4.1.5 Andrew安全RPC协议 63

4.2 具有可信第三方的对称密钥协议 63

4.2.1 NSSK协议 63

4.2.2 Otway-Rees协议 64

4.2.3 Yahalom协议 65

4.2.4 大嘴青蛙协议 65

4.2.5 Denning Sacco协议 66

4.2.6 Woo-Lam协议 66

4.3 无可信第三方的公开密钥协议 67

4.3.1 ISO one-pass公开密钥单向认证协议 67

4.3.2 ISO two-pass公开密钥单向认证协议 67

4.3.3 ISO two-pass公开密钥双向认证协议 68

4.3.4 ISO three-pass公开密钥双向认证协议 68

4.3.5 ISO two-pass公开密钥并行双向认证协议 68

4.3.6 Diffie-Hellman协议 68

4.4 具有可信第三方的公开密钥协议 69

4.4.1 NSPK协议 69

4.4.2 SPLICE/AS协议 70

4.4.3 Denning Sacco密钥分配协议 71

4.5 针对认证与密钥交换协议的攻击 71

4.5.1 针对无可信第三方的对称密钥协议的攻击 71

4.5.2 针对具有可信第三方的对称密钥协议的攻击 72

4.5.3 针对无可信第三方的公开密钥协议的攻击 76

4.5.4 针对具有可信第三方的公开密钥协议的攻击 77

4.6 本章小结 79

习题 79

第5章 电子商务协议 80

5.1 电子商务协议概述 80

5.1.1 电子商务协议研究背景 80

5.1.2 电子商务协议的安全属性 81

5.2 非否认协议 82

5.2.1 非否认协议的基本概念 82

5.2.2 Markowitch和Roggeman协议 83

5.2.3 Zhou-Gollmann协议 84

5.2.4 Online TTP非否认协议——CMP1协议 86

5.3 电子现金协议 87

5.3.1 电子现金协议中的密码技术 87

5.3.2 Digicash电子现金协议 91

5.3.3 Brands电子现金协议 92

5.4 电子支付协议 94

5.4.1 First Virtual协议 94

5.4.2 Net Bill协议 95

5.4.3 ISI协议 96

5.4.4 iKP协议 97

5.4.5 IBS协议 100

5.4.6 SSL协议 101

5.4.7 SET协议 101

5.5 安全电子邮件协议 102

5.6 本章小结 103

习题 104

第6章 实际使用中的安全协议 105

6.1 Kerberos协议 105

6.1.1 概述 105

6.1.2 术语 106

6.1.3 运行环境 106

6.1.4 消息交互 107

6.1.5 跨域认证 110

6.1.6 安全性分析 111

6.2 SSL协议 112

6.2.1 概述 112

6.2.2 特点 113

6.2.3 结构 114

6.2.4 原理 115

6.2.5 安全性分析 118

6.3 IPSec协议 119

6.3.1 概述 119

6.3.2 结构 120

6.3.3 认证头协议 121

6.3.4 封装安全载荷协议 122

6.3.5 AH协议及ESP协议的工作模式 124

6.3.6 Internet密钥交换协议 125

6.3.7 安全性分析 128

6.4 Set协议 130

6.4.1 概述 130

6.4.2 SET支付模型 131

6.4.3 交易流程 132

6.4.4 证书管理 137

6.4.5 安全性分析 140

6.5 本章小结 142

习题 143

第三部分 安全协议的分析、验证方法第7章 BAN逻辑 147

7.1 BAN逻辑的基本框架 147

7.1.1 BAN逻辑的语法、语义 148

7.1.2 BAN逻辑的推理规则 149

7.2 应用BAN逻辑分析协议的方法 151

7.2.1 理想化过程 151

7.2.2 认证协议的基本假设 151

7.2.3 协议解释 152

7.2.4 形式化协议目标 152

7.2.5 BAN逻辑协议分析步骤 153

7.3 BAN逻辑的应用实例 153

7.3.1 应用BAN逻辑分析Otway-Rees协议 153

7.3.2 应用BAN逻辑分析NS对称密钥协议 157

7.3.3 应用BAN逻辑分析NS公开密钥协议 160

7.4 BAN逻辑的缺陷 164

7.4.1 BAN逻辑的缺陷 164

7.4.2 BAN逻辑的改进方向 167

7.5 本章小结 167

习题 167

第8章 BAN类逻辑 168

8.1 GNY逻辑 168

8.1.1 GNY逻辑的计算模型 169

8.1.2 GNY逻辑的语法、语义 169

8.1.3 GNY逻辑的推理规则 170

8.1.4 GNY逻辑应用实例 174

8.2 AT逻辑 177

8.2.1 AT逻辑的语法 179

8.2.2 AT逻辑的推理规则 180

8.2.3 AT逻辑的计算模型 181

8.2.4 AT逻辑的语义 182

8.3 SVO逻辑 185

8.3.1 SVO逻辑的语法 185

8.3.2 SVO逻辑的推理规则 186

8.3.3 计算模型 187

8.3.4 SVO逻辑的语义 188

8.3.5 SVO逻辑的应用实例 190

8.4 本章小结 196

习题 197

第9章 Kailar逻辑 198

9.1 电子商务协议的安全性分析 198

9.1.1 匿名性 199

9.1.2 原子性 199

9.1.3 不可否认性 199

9.1.4 可追究性 200

9.1.5 公平性 200

9.2 Kailar逻辑的基本构件 201

9.3 Kailar逻辑的推理规则 202

9.3.1 一般推理规则 202

9.3.2 可追究性推理规则 203

9.4 Kailar逻辑的应用举例 203

9.4.1 IBS协议 203

9.4.2 CMP1协议 206

9.4.3 ISI协议 208

9.5 Kailar逻辑的缺陷 210

9.6 本章小结 212

习题 212

第10章 时间相关安全协议分析 213

10.1 Timed Release密码协议 213

10.2 CS逻辑的逻辑构件 215

10.3 CS逻辑的推理规则 216

10.4 CS逻辑的公理 216

10.5 CS逻辑的应用分析 217

10.6 CS逻辑的改进 220

10.6.1 修改密文公理 221

10.6.2 修改消息接收公理 222

10.6.3 时间密钥 222

10.7 改进的CS逻辑的应用分析 223

10.7.1 时间标注 224

10.7.2 协议目标 224

10.7.3 初始假设 225

10.7.4 协议分析 225

10.8 本章小结 228

习题 228

第11章 串空间模型理论及协议分析方法 229

11.1 串空间模型理论基础 230

11.1.1 基本概念 230

11.1.2 丛和结点的因果依赖关系 232

11.1.3 攻击者描述 233

11.1.4 协议正确性概念 237

11.2 基于极小元理论的串空间方法 237

11.2.1 NSL串空间 237

11.2.2 NSL响应者的一致性 238

11.2.3 响应者的秘密性 241

11.2.4 NSL发起者的秘密性 242

11.2.5 NSL发起者的一致性 242

11.3 理想与诚实理论 243

11.3.1 理想 243

11.3.2 诚实 244

11.4 基于理想与诚实理论的串空间方法 246

11.4.1 Otway-Rees协议的串空间模型 246

11.4.2 机密性 247

11.4.3 认证性 248

11.5 认证测试理论 250

11.5.1 基本概念 251

11.5.2 攻击者密钥和安全密钥 251

11.5.3 认证测试 252

11.6 基于认证测试理论的串空间方法 254

11.6.1 Otway-Rees协议的串空间模型 254

11.6.2 Otway-Rees协议认证 254

11.7 串空间理论分析方法的比较 256

11.8 本章小结 256

习题 257

第12章 安全协议的CSP分析方法 258

12.1 CSP基本概念 258

12.1.1 事件 258

12.1.2 进程 259

12.1.3 迹 261

12.1.4 并发 264

12.1.5 选择 265

12.1.6 穿插 266

12.1.7 CSP建模举例 266

12.2 安全属性 268

12.2.1 秘密性 269

12.2.2 认证性 269

12.3 CSP网络模型 270

12.3.1 网络模型 270

12.3.2 消息空间 271

12.3.3 攻击者描述 272

12.3.4 协议参与者 274

12.4 CSP方法的应用分析 274

12.4.1 消息空间 274

12.4.2 协议建模 274

12.4.3 协议分析 275

12.5 本章小结 278

习题 278

第13章 其他安全协议分析验证方法 279

13.1 Dolev-Yao模型 279

13.1.1 协议模型 280

13.1.2 协议安全的定义 280

13.1.3 举例 281

13.2 Paulson归纳法 282

13.2.1 归纳定义操作 282

13.2.2 事件和攻击者 283

13.2.3 协议建模 283

13.2.4 标准规则 284

13.2.5 归纳法 285

13.2.6 证明秘密性定理 285

13.3 Schneider秩函数 286

13.3.1 基本概念 286

13.3.2 实例分析 288

13.4 基于Petri网的安全协议分析方法 291

13.4.1 基本概念 291

13.4.2 协议建模 293

13.4.3 带攻击者的协议建模 294

13.4.4 攻击者模型 295

13.4.5 安全属性分析 298

13.5 本章小结 300

习题 300

参考文献 301