图书介绍

密码协议分析的逻辑方法pdf电子书版本下载

密码协议分析的逻辑方法
  • 雷新锋,薛锐著 著
  • 出版社: 北京:科学出版社
  • ISBN:9787030370969
  • 出版时间:2013
  • 标注页数:381页
  • 文件大小:127MB
  • 文件页数:396页
  • 主题词:密码协议-逻辑方法

PDF下载


点此进入-本书在线PDF格式电子书下载【推荐-云解压-方便快捷】直接下载PDF格式图书。移动端-PC端通用
种子下载[BT下载速度快] 温馨提示:(请使用BT下载软件FDM进行下载)软件下载地址页 直链下载[便捷但速度慢]   [在线试读本书]   [在线获取解压码]

下载说明

密码协议分析的逻辑方法PDF格式电子书版下载

下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。

建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台)。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如 BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用!后期资源热门了。安装了迅雷也可以迅雷进行下载!

(文件页数 要大于 标注页数,上中下等多册电子书除外)

注意:本站所有压缩包均有解压码: 点击下载压缩包解压工具

图书目录

第一部分 理论基础 3

第1章 数理逻辑基础 3

1.1 基本概念 3

1.2 命题逻辑 5

1.2.1 命题逻辑语法 5

1.2.2 命题逻辑语义 6

1.2.3 命题逻辑推演系统 7

1.2.4 命题逻辑的可靠性 8

1.3 谓词逻辑 9

1.3.1 谓词逻辑语法 9

1.3.2 谓词逻辑的语义 11

1.3.3 谓词逻辑推演系统 13

1.3.4 谓词逻辑的可靠性 13

1.4 模态逻辑 13

1.4.1 命题模态逻辑 14

1.4.2 谓词模态逻辑 17

1.4.3 知识逻辑与信念逻辑 19

1.5 Hoare逻辑 20

1.6 本章小结 21

参考文献 21

第2章 现代密码学基础 23

2.1 概述 23

2.1.1 加密方案 23

2.1.2 对加密方案的攻击 24

2.1.3 信息论安全 24

2.1.4 现代密码学 25

2.2 计算复杂性 26

2.2.1 图灵机 26

2.2.2 时间复杂性 27

2.2.3 P与NP 28

2.2.4 多项式时间归约 28

2.2.5 概率图灵机与BPP 29

2.3 计算安全 30

2.3.1 计算安全的概念 30

2.3.2 安全假设 31

2.3.3 几个安全相关概念 32

2.4 私钥加密 33

2.4.1 私钥加密方案 33

2.4.2 私钥加密方案的CPA安全 34

2.4.3 私钥加密方案的CCA安全 35

2.5 公钥加密 35

2.5.1 公钥加密方案 36

2.5.2 公钥加密方案的CPA安全 36

2.5.3 公钥加密方案的CCA安全 37

2.6 数字签名 37

2.6.1 数字签名方案 38

2.6.2 数字签名方案的安全性 38

2.7 安全性证明 39

2.7.1 概率多项式时间归约 39

2.7.2 混合论证 40

2.7.3 标准模型与随机应答器模型 40

2.8 本章小结 41

参考文献 42

第二部分 密码协议分析概述 45

第3章 密码协议 45

3.1 密码协议的概念与意义 45

3.2 密码协议的属性与分类 46

3.3 对密码协议的攻击 47

3.4 密码协议的表示法 50

3.5 密码协议实例 51

3.6 本章小结 59

参考文献 60

第4章 密码协议分析 61

4.1 形式化方法 61

4.1.1 形式化方法概览 61

4.1.2 DY模型 64

4.1.3 Woo-Lam模型及其扩展 66

4.2 计算方法 67

4.2.1 计算方法概览 67

4.2.2 BR模型 68

4.2.3 其他模型 71

4.3 密码协议形式化分析的计算可靠性 71

4.3.1 基于映射的方法 72

4.3.2 基于模拟的方法 73

4.3.3 已有形式化方法的计算可靠性 73

4.3.4 计算方法的直接形式化 74

4.4 可复合密码协议分析 75

4.5 密码协议逻辑 76

4.6 本章小结 77

参考文献 77

第三部分 密码协议逻辑 87

第5章 BAN逻辑 87

5.1 BAN逻辑的语法 87

5.2 推理规则 88

5.3 协议及其目标的描述 92

5.3.1 协议理想化 92

5.3.2 协议注解 93

5.3.3 认证目标的形式化 94

5.4 协议分析实例 95

5.4.1 NSSK协议及其形式化分析 95

5.4.2 Kerberos协议及其形式化分析 98

5.5 对BAN逻辑语义的简单讨论 101

5.6 对BAN逻辑的不同意见 103

5.6.1 Nessett的评论 103

5.6.2 Snekkenes的评论 105

5.7 本章小结 107

参考文献 107

第6章 BAN逻辑的扩展 108

6.1 GNY逻辑 108

6.1.1 模型 108

6.1.2 GNY逻辑的语法 109

6.1.3 推理规则 111

6.1.4 协议形式化 117

6.1.5 协议分析实例 118

6.2 VO逻辑 123

6.2.1 语法扩展 123

6.2.2 公理与规则扩展 125

6.2.3 通用的形式化目标 125

6.2.4 通用的形式化假设 127

6.2.5 STS协议分析 127

6.3 MB逻辑 130

6.3.1 公式 131

6.3.2 推理规则 132

6.3.3 协议消息理想化 134

6.3.4 协议分析 135

6.4 本章小结 136

参考文献 137

第7章 类BAN逻辑的语义 138

7.1 AT逻辑 138

7.1.1 AT逻辑对BAN逻辑的改进 138

7.1.2 语法 141

7.1.3 公理系统 142

7.1.4 模型 143

7.1.5 AT逻辑的语义 145

7.2 SVO逻辑 148

7.2.1 SVO逻辑语言 148

7.2.2 公理系统 149

7.2.3 模型 152

7.2.4 SVO逻辑的语义 154

7.2.5 SVO逻辑的可靠性 158

7.2.6 基于SVO逻辑的协议分析 159

7.3 本章小结 162

参考文献 163

第8章 BAN逻辑的进一步扩展 164

8.1 Kailar逻辑 164

8.1.1 可追责性 164

8.1.2 分析框架 165

8.1.3 分析假设 166

8.1.4 逻辑规则 167

8.1.5 协议目标 169

8.1.6 分析实例 169

8.2 BSW逻辑 171

8.2.1 模型 172

8.2.2 BSW逻辑语言 173

8.2.3 推理规则 174

8.2.4 定理 175

8.2.5 合成规则 175

8.2.6 协议分析与设计的实例 177

8.3 本章小结 181

参考文献 181

第9章 非单调逻辑 182

9.1 引言 182

9.2 Moser逻辑 182

9.2.1 知道与相信公理 183

9.2.2 unless谓词 184

9.2.3 关于unless的例子 185

9.3 Rubin逻辑 186

9.3.1 khat协议 186

9.3.2 协议描述与分析概述 187

9.3.3 全局集 188

9.3.4 本地集 189

9.3.5 信任矩阵 190

9.3.6 行为描述 191

9.3.7 更新函数 193

9.3.8 推理规则 194

9.3.9 对khat协议的描述与分析 195

9.4 本章小结 199

参考文献 200

第10章 引入时间的协议逻辑 201

10.1 CKT5逻辑 201

10.1.1 CKT5逻辑术语 202

10.1.2 安全性定理 205

10.2 CS逻辑 208

10.2.1 语法 208

10.2.2 公理与推理规则 209

10.2.3 实例分析 211

10.3 GS逻辑 213

10.3.1 扩展术语及规则 214

10.3.2 协议分析实例 215

10.4 本章小结 218

参考文献 218

第11章 时间相关密码协议逻辑及其形式化语义 220

11.1 TCPL的引入 220

11.2 TCPL的语法 222

11.3 公理与规则 225

11.4 TCPL的语义 228

11.4.1 模型 228

11.4.2 语义 232

11.5 TCPL的可靠性 233

11.6 基于TCPL的密码协议形式化建模方案 238

11.6.1 密码协议建模 238

11.6.2 安全属性建模 241

11.7 基于TCPL的密码协议分析 243

11.7.1 定时发布协议 243

11.7.2 NSPK协议 249

11.8 进步讨论 250

11.9 本章小结 252

参考文献 252

第12章 协议复合逻辑 255

12.1 协议编程语言 255

12.1.1 PPL的语法 255

12.1.2 PPL的语义 258

12.2协议及其属性 259

12.2.1 协议执行模型 259

12.2.2 协议属性 260

12.3 PCL的语法与语义 261

12.3.1 PCL的语法 261

12.3.2 PCL的语义 262

12.4 证明系统 264

12.5 PCL的可靠性 267

12.6 协议分析实例 270

12.6.1 弱认证 270

12.6.2 强认证性 271

12.7 协议复合 272

12.7.1 并行复合 272

12.7.2 顺序复合 273

12.7.3 协议复合实例 274

12.8 PCL协议存在的问题 275

12.9 本章小结 276

参考文献 276

第四部分 计算可靠的密码协议逻辑 281

第13章 AR逻辑 281

13.1 形式化加密与消息等价 281

13.1.1 形式化消息 281

13.1.2 消息等价 282

13.2 加密方案与不可区分性 284

13.2.1 加密方案的安全性 284

13.2.2 加密方案安全性的定义 285

13.3 形式等价的计算可靠性 286

13.3.1 总体关联 287

13.3.2 等价性蕴涵不可区分性 287

13.4 不完备性 293

13.5 完备性定理 295

13.5.1 无混淆加密与认证加密 296

13.5.2 完备性定理 297

13.6 本章小结 305

参考文献 306

第14章 对AR逻辑的扩展 307

14.1 形式化模型 308

14.1.1 消息 308

14.1.2 模式 310

14.1.3 等价 313

14.2 计算模型 315

14.3 计算可靠性 317

14.4 本章小结 324

参考文献 325

第15章 计算可靠的PCL 327

15.1 协议语法 327

15.2 逻辑语法 328

15.3 证明系统 329

15.4 证明实例 330

15.5 协议的执行 331

15.6 计算语义 333

15.7 本章小结 336

参考文献 336

第16章 IK逻辑 337

16.1 T系统 338

16.1.1 语法 340

16.1.2 T系统的公理 341

16.1.3 T系统的可靠性 345

16.2 基于T系统的实例证明 345

16.3 计算不可区分系统 348

16.3.1 语法 348

16.3.2 证明规则 349

16.4 基于IK逻辑的证明实例 350

16.5 IK逻辑的可靠性 351

16.6 本章小结 352

参考文献 353

第17章 计算不可区分逻辑 354

17.1 应答器系统 354

17.1.1 应答器系统与敌手 354

17.1.2 语义 357

17.1.3 事件 358

17.2 CIL的语句与基本规则 359

17.2.1 语句 359

17.2.2 基本规则 359

17.3 上下文 360

17.4 互模拟 362

17.5 确定性 364

17.6 CIL的规则与可靠性 364

17.6.1 上下文与应答器规则 364

17.6.2 派生规则与外部前提 365

17.7 概率签名方案 366

17.7.1 随机应答器 367

17.7.2 形式化证明 368

17.8 本章小结 372

参考文献 373

结束语 374

索引 377

精品推荐