安全协议原理与验证PDF|Epub|txt|kindle电子书版本网盘下载

安全协议原理与验证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 数据加密标准DES19

2.3.3 高级数据加密标准AES27

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