近20年来，安全协定技术及套用飞速发展，是通信及计算机学科的热门课题。无论是在学术界还是在工程套用方面都得到了前所未有的重视。本书主要介绍安全协定设计準则与分析方法，其中包括安全协定研究背景和设计準则、逻辑化分析方法、串空间方法及可证明安全性方法等，同时给出了利用各种方法分析安全协定的具体实例。

本书可作为计算机、通信及信息安全专业的高年级选修教材，也可作为相关专业的研究生教材。同时还可作为该领域工程技术人员学习安全协定的参考书。

第1章 绪论1

1.1 安全协定的背景1

1.2 安全协定及分类 2

1.3 安全协定面临的威胁3

1.4 安全协定设计4

1.5 安全协定分析方法概述4

参考文献5

第2章 安全协定的逻辑化分析方法7

2.1 BAN逻辑7

2.1.1 BAN逻辑的基本命题符号7

2.1.2 BAN逻辑的公理系统8

2.1.3 BAN逻辑的使用方法9

2.1.4 BAN逻辑的优点和不足13

2.2 GNY逻辑14

2.2.1 GNY逻辑的语义14

2.2.2 GNY逻辑公理15

2.3 SVO逻辑18

2.3.1 SVO逻辑的语义18

2.3.2 SVO逻辑的公理系统19

2.4 AT逻辑20

2.4.1 AT逻辑语义20

2.4.2 AT逻辑的公理系统21

2.5 Rubin逻辑23

2.5.1 Rubin逻辑语义23

2.5.2 Rubin逻辑的公理系统26

2.5.3 扩展的Rubin逻辑26

2.6 ZWW逻辑28

2.6.1 ZWW语义28

2.6.2 永真公式集合Γ和推理规则29

2.6.3 ZWW逻辑套用示例31

2.7 SPALL逻辑33

2.7.1 若干基本概念34

2.7.2 讯息及其相关概念36

2.7.3 公式及其相关概念37

2.7.4 SPALL 的公理系统42

2.7.5 SPALL系统的若干定理44

2.7.6 SPALL系统套用示例50

2.7.7 对SPALL逻辑的几点说明60

参考文献61

第3章 安全协定的串空间分析方法62

3.1 串与串空间的概念62

3.1.1 项与子项62

3.1.2 串和串空间63

3.1.3 丛与因果先后次序65

3.2 入侵串68

3.2.1 入侵串与可获取密钥及安全密钥68

3.2.2 理想与诚实69

3.3 认证测试及其套用71

3.3.1 认证测试71

3.3.2 套用实例73

3.4 注记75

参考文献76

第4章 可证明安全性分析方法77

4.1 引言77

4.2 可证明安全性的三大基本原则78

4.2.1 严格準确的安全定义79

4.2.2 可準确描述的安全假设80

4.2.3 形式化的安全性证明80

4.3 密码学标準假设81

4.3.1 常用定义与表示法81

4.3.2 离散对数假设与Diffie-Hellman假设82

4.4 协定分析实例：Diffie-Hellman 密钥交换协定82

4.4.1 安全模型与安全定义83

4.4.2 Diffie-Hellman 密码交换协定84

4.5 随机预言机模型86

4.6 基于博弈序列的安全性证明方法87

4.6.1 基本思路88

4.6.2 证明实例:ElGamal 加密体制89

4.7 泛组合方法92

4.7.1 互动式图灵机与分布不可区分92

4.7.2 UC模型下协定的安全性95

4.8 小结101

参考文献101

第5章 基于中心伺服器认证的密钥交换协定103

5.1 引言103

5.2 Canetti-Krawczyk模型104

5.2.1 协定会话105

5.2.2 非认证链路攻击模型105

5.2.3 认证链路攻击模型107

5.2.4 证明实例：Diffie-Hellman协定108

5.3 扩展Canetti-Krawczyk模型110

5.3.1 设计动机110

5.3.2 模型描述111

5.3.3 攻击SIG-DH协定113

5.4 MQV类协定114

5.4.1 协定构造及相关变型114

5.4.2 安全证明123

5.5 其他的协定构造方式127

5.5.1 NAXOS技术127

5.5.2 伪静态密钥与滞后临时密钥技术128

5.6 小结130

参考文献131

第6章 基于口令的认证密钥交换协定133

6.1 引言133

6.2 非对称口令认证密钥交换协定134

6.2.1 协定安全模型与必要的密码学假设135

6.2.2 HK协定及其安全证明 137

6.3 Bellare-Pointcheval-Rogaway模型143

6.3.1 BPR模型的参与者描述143

6.3.2 BPR模型攻击者的定义143

6.3.3 BPR模型安全的定义146

6.4 一次加密密钥交换协定147

6.4.1 协定描述148

6.4.2 语义安全149

6.4.3 安全证明149

6.5 小结154

参考文献155

第7章 RFID协定设计与分析156

7.1 引言156

7.2 RFID系统与相关的安全问题158

7.2.1 RFID系统组成158

7.2.2 RFID工作原理160

7.2.3 RFID相关的安全问题161

7.3 RFID认证协定的各种攻击方法163

7.3.1 RFID认证协定主要的攻击方法163

7.3.2 一些RFID认证协定的安全性分析164

7.3.3 RFID认证协定的安全需求177

7.4 轻型RFID认证协定的设计179

7.4.1 基本设计原则179

7.4.2 Yoon等人的RFID认证协定安全性新分析181

7.4.3 一个轻型RFID协定的设计与分析183

7.5 RFID协定的前向安全性184

7.5.1 前向安全性的重要性184

7.5.2 前向安全性协定的一般设计方法185

7.5.3 一类协定的新分析及改进186

7.6 HBN协定的设计与分析191

7.6.1 HB类协定的研究进展192

7.6.2 LPN问题与HB类协定192

7.6.3 HB类协定的一些可证明安全规约结果195

7.6.4 HB类协定主要的攻击方法197

7.6.5 HBN协定的设计与分析198

参考文献199