安全协议设计与分析

第1章 绪论
1．1 安全协议的背景
1．2 安全协议及分类
1．3 安全协议面临的威胁
1．4 安全协议设计
1．5 安全协议分析方法概述
参考文献
第2章 安全协议的逻辑化分析方法
2．1 BAN逻辑
2．1．1 BAN逻辑的基本命题符号
2．1．2 BAN逻辑的公理系统
2．1．3 BAN逻辑的使用方法
2．1．4 BAN逻辑的优点和不足
2．2 GNY逻辑
2．2．1 GNY逻辑的语义
2．2．2 GNY逻辑公理
2．3 SVO逻辑
2．3．1 SVO逻辑的语义
2．3．2 SVO逻辑的公理系统
2．4 AT逻辑
2．4．1 AT逻辑语义
2．4．2 AT逻辑的公理系统
2．5 Rubin逻辑
2．5．1 Rubin逻辑语义
2．5．2 Rubin逻辑的公理系统
2．5．3 扩展的Rubin逻辑
2．6 ZWW逻辑
2．6．ZWW语义
2．6．2 永真公式集合厂和推理规则
2．6．3 ZWW逻辑应用示例
2．7 SPALL逻辑
2．7．1 若干基本概念
2．7．2 消息及其相关概念
2．7．3 公式及其相关概念
2．7．4 SPALL的公理系统
2．7．5 SPALL系统的若干定理
2．7．6 SPALL系统应用示例
2．7．7 对SPALL逻辑的几点说明
参考文献
第3章 安全协议的串空间分析方法
3．1 串与串空间的概念
3．1．1 项与子项
3．1．2 串和串空间
3．1．3 丛与因果先后次序
3．2 入侵串
3．2．1 入侵串与可获取密钥及安全密钥
3．2．2 理想与诚实
3．3 认证测试及其应用
3．3．1 认证测试
3．3．2 应用实例
3．4 注记
参考文献
第4章 可证明安全性分析方法
4．1 引言
4．2 可证明安全性的三大基本原则
4．2．1 严格准确的安全定义
4．2．2 可准确描述的安全假设
4．2．3 形式化的安全性证明
4．3 密码学标准假设
4．3．1 常用定义与表示法
4．3．2 离散对数假设与Diffie-Hellman假设
4．4 协议分析实例：DiffieRFIDHellman密钥交换协议
4．4．1 安全模型与安全定义
4．4．2 DiffieRFIDHeIlman密码交换协议
4．5 随机预言机模型
4．6 基于博弈序列的安全性证明方法
4．6．1 基本思路
4．6．2 证明实例：ElGamal加密体制
4．7 泛组合方法
4．7．1 交互式图灵机与分布不可区分
4．7．2 UC模型下协议的安全性
4．8 小结
参考文献
第5章 基于中心服务器认证的密钥交换协议
5．1 引言
5．2 Canetti-Krawczyk模型
5．2．1 协议会话
5．2．2 非认证链路攻击模型
5．2．3 认证链路攻击模型
5．2．4 证明实例：Diffie-Hellman协议
5．3 扩展Canetti-Krawczyk模型
5．3．1 设计动机
5．3．2 模型描述
5．3．3 攻击SIG-DH协议
5．4 MQV类协议
5．4．1 协议构造及相关变型
5．4．2 安全证明
5．5 其他的协议构造方式
5．5．1 NAXOS技术
5．5．2 伪静态密钥与滞后临时密钥技术
5．6 小结
参考文献
第6章 基于口令的认证密钥交换协议
6．1 引言
6．2 非对称口令认证密钥交换协议
6．2．1 协议安全模型与必要的密码学假设
6．2．2 HK协议及其安全证明
6．3 Bellare-Pointcheval-Rogaway模型
6．3．1 BPR模型的参与者描述
6．3．2 BPR模型攻击者的定义
6．3．3 BPR模型安全的定义
6．4 一次加密密钥交换协议
6．4．1 协议描述
6．4．2 语义安全
6．4．3 安全证明
6．5 小结
参考文献
第7章 RFID协议设计与分析
7．1 引言
7．2 RFID系统与相关的安全问题
7．2．1 RFID系统组成
7．2．2 RFID工作原理
7．2．3 RFID相关的安全问题
7．3 RFID认证协议的各种攻击方法
7．3．1 RFID认证协议主要的攻击方法
7．3．2 一些RFID认证协议的安全性分析
7．3．3 RFID认证协议的安全需求
7．4 轻型RFID认证协议的设计
7．4．1 基本设计原则
7．4．2 Yoon等人的RFID认证协议安全性新分析
7．4．3 一个轻型RFID协议的设计与分析
7．5 RFID协议的前向安全性
7．5．1 前向安全性的重要性
7．5．2 前向安全性协议的一般设计方法
7．5．3 一类协议的新分析及改进
7．6 HBN协议的设计与分析
7．6．1 HB类协议的研究进展
7．6．2 LPN问题与HB类协议
7．6．3 HB类协议的一些可证明安全规约结果
7．6．4 HB类协议主要的攻击方法
7．6．5 HBN协议的设计与分析
参考文献