密码协议分析的逻辑方法
内容简介
对密码协议分析的逻辑方法进行系统介绍。主要内容包括密码协议的概念以及密码协议分析的主要方法综述，密码协议逻辑分析方法的理论基础，各种密码协议逻辑。这些逻辑涵盖了当前比较重要的密码协议分析逻辑，介绍了基于逻辑的计算可靠性的分析方法.重点介绍了作者在密码协议分析的逻辑方面进行的工作.
目录
前言
第1部分 理论基础
第1章 数理逻辑基础
1.1 基本概念
1.2 命题逻辑
1.2.1 命题逻辑语法
1.2.2 命题逻辑语义
1.2.3 命题逻辑推演系统
1.2.4 命题逻辑的可靠性
1.3 谓词逻辑
1.3.1 谓词逻辑语法
1.3.2 谓词逻辑的语义
1.3.3 谓词逻辑推演系统
1.3.4 谓词逻辑的可靠性
1.4 模态逻辑
1.4.1 命题模态逻辑
1.4.2 谓词模态逻辑
1.4.3 知识逻辑与信念逻辑
1.5 Hoare逻辑
1.6 本章小结
参考文献
第2章 现代密码学基础
2.1 概述
2.1.1 加密方案
2.1.2 对加密方案的攻击
2.1.3 信息论安全
2.1.4 现代密码学
2.2 计算复杂性
2.2.1 图灵机
2.2.2 时间复杂性
2.2.3 P与NP
2.2.4 多项式时间归约
2.2.5 概率图灵机与BPP
2.3 计算安全
2.3.1 计算安全的概念
2.3.2 安全假设
2.3.3 几个安全相关概念
2.4 私钥加密
2.4.1 私钥加密方案
2.4.2 私钥加密方案的CPA安全
2.4.3 私钥加密方案的CCA安全
2.5 公钥加密
2.5.1 公钥加密方案
2.5.2 公钥加密方案的CPA安全
2.5.3 公钥加密方案的CCA安全
2.6 数字签名
2.6.1 数字签名方案
2.6.2 数字签名方案的安全性
2.7 安全性证明
2.7.1 概率多项式时间归约
2.7.2 混合论证
2.7.3 标准模型与随机应答器模型
2.8 本章小结
参考文献
第二部分 密码协议分析概述
第3章 密码协议
3.1 密码协议的概念与意义
3.2 密码协议的属性与分类
3.3 对密码协议的攻击
3.4 密码协议的表示法
3.5 密码协议实例
3.6 本章小结
参考文献
第4章 密码协议分析
4.1 形式化方法
4.1.1 形式化方法概览
4.1.2 DY模型
4.1.3 Woo-Lam模型及其扩展
4.2 计算方法
4.2.1 计算方法概览
4.2.2 BR模型
4.2.3 其他模型
4.3 密码协议形式化分析的计算可靠性
4.3.1 基于映射的方法
4.3.2 基于模拟的方法
4.3.3 已有形式化方法的计算可靠性
4.3.4 计算方法的直接形式化
4.4 可复合密码协议分析
4.5 密码协议逻辑
4.6 本章小结
参考文献
第三部分 密码协议逻辑
第5章 BAN逻辑
5.1 BAN逻辑的语法
5.2 推理规则
5.3 协议及其目标的描述
5.3.1 协议理想化
5.3.2 协议注解
5.3.3 认证目标的形式化
5.4 协议分析实例
5.4.1 NSSK协议及其形式化分析
5.4.2 Kerberos协议及其形式化分析
5.5 对BAN逻辑语义的简单讨论
5.6 对BAN逻辑的不同意见
5.6.1 Nessett的评论
5.6.2 Snekkenes的评论
5.7 本章小结
参考文献
第6章 BAN逻辑的扩展
6.1 GNY逻辑
6.1.1 模型
6.1.2 GNY逻辑的语法
6.1.3 推理规则
6.1.4 协议形式化
6.1.5 协议分析实例
6.2 VO逻辑
6.2.1 语法扩展
6.2.2 公理与规则扩展
6.2.3 通用的形式化目标
6.2.4 通用的形式化假设
6.2.5 STS协议分析
6.3 MB逻辑
6.3.1 公式
6.3.2 推理规则
6.3.3 协议消息理想化
6.3.4 协议分析
6.4 本章小结
参考文献
第7章 类BAN逻辑的语义
7.1 AT逻辑
7.1.1 AT逻辑对BAN逻辑的改进
7.1.2 语法
7.1.3 公理系统
7.1.4 模型
7.1.5 AT逻辑的语义
7.2 SVO逻辑
7.2.1 SVO逻辑语言
7.2.2 公理系统
7.2.3 模型
7.2.4 SVO逻辑的语义
7.2.5 SVO逻辑的可靠性
7.2.6 基于SVO逻辑的协议分析
7.3 本章小结
参考文献
第8章 BAN逻辑的进一步扩展
8.1 Kailar逻辑
8.1.1 可追责性
8.1.2 分析框架
8.1.3 分析假设
8.1.4 逻辑规则
8.1.5 协议目标
8.1.6 分析实例
8.2 BSW逻辑
8.2.1 模型
8.2.2 BSW逻辑语言
8.2.3 推理规则
8.2.4 定理
8.2.5 合成规则
8.2.6 协议分析与设计的实例
8.3 本章小结
参考文献
第9章 非单调逻辑
9.1 引言
9.2 Moser逻辑
9.2.1 知道与相信公理
9.2.2 unless谓词
9.2.3 关于unless的例子
9.3 Rubin逻辑
9.3.1 khat协议
9.3.2 协议描述与分析概述
9.3.3 全局集
9.3.4 本地集
9.3.5 信任矩阵
9.3.6 行为描述
9.3.7 更新函数
9.3.8 推理规则
9.3.9 对khat协议的描述与分析
9.4 本章小结
参考文献
第10章 引入时间的协议逻辑
10.1 CKT5逻辑
10.1.1 CKT5逻辑术语
10.1.2 安全性定理
10.2 CS逻辑
10.2.1 语法
10.2.2 公理与推理规则
10.2.3 实例分析
10.3 GS逻辑
10.3.1 扩展术语及规则
10.3.2 协议分析实例
10.4 本章小结
参考文献
第11章 时间相关密码协议逻辑及其形式化语义
11.1 TCPL的引入
11.2 TCPL的语法
11.3 公理与规则
11.4 TCPL的语义
11.4.1 模型
11.4.2 语义
11.5 TCPL的可靠性
11.6 基于TCPL的密码协议形式化建模方案
11.6.1 密码协议建模
11.6.2 安全属性建模
11.7 基于TCPL的密码协议分析
11.7.1 定时发布协议
11.7.2 NSPK协议
11.8 进一步讨论
11.9 本章小结
参考文献
第12章 协议复合逻辑
12.1 协议编程语言
12.1.1 PPL的语法
12.1.2 PPL的语义
12.2 协议及其属性
12.2.1 协议执行模型
12.2.2 协议属性
12.3 PCL的语法与语义
12.3.1 PCL的语法
12.3.2 PCL的语义
12.4 证明系统
12.5 PCL的可靠性
12.6 协议分析实例
12.6.1 弱认证
12.6.2 强认证性
12.7 协议复合
12.7.1 并行复合
12.7.2 顺序复合
12.7.3 协议复合实例
12.8 PCL协议存在的问题
12.9 本章小结
参考文献
第四部分 计算可靠的密码协议逻辑
第13章 AR逻辑
13.1 形式化加密与消息等价
13.1.1 形式化消息
13.1.2 消息等价
13.2 加密方案与不可区分性
13.2.1 加密方案的安全性
13.2.2 加密方案安全性的定义
13.3 形式等价的计算可靠性
13.3.1 总体关联
13.3.2 等价性蕴涵不可区分性
13.4 不完备性
13.5 完备性定理
13.5.1 无混淆加密与认证加密
13.5.2 完备性定理
13.6 本章小结
参考文献
第14章 对AR逻辑的扩展
14.1 形式化模型
14.1.1 消息
14.1.2 模式
14.1.3 等价
14.2 计算模型
14.3 计算可靠性
14.4 本章小结
参考文献
第15章 计算可靠的PCL
15.1 协议语法
15.2 逻辑语法
15.3 证明系统
15.4 证明实例
15.5 协议的执行
15.6 计算语义
15.7 本章小结
参考文献
第16章 IK逻辑
16.1 T系统
16.1.1 语法
16.1.2 T系统的公理
16.1.3 T系统的可靠性
16.2 基于T系统的实例证明
16.3 计算不可区分系统
16.3.1 语法
16.3.2 证明规则
16.4 基于IK逻辑的证明实例
16.5 IK逻辑的可靠性
16.6 本章小结
参考文献
第17章 计算不可区分逻辑
17.1 应答器系统
17.1.1 应答器系统与敌手
17.1.2 语义
17.1.3 事件
17.2 CIL的语句与基本规则
17.2.1 语句
17.2.2 基本规则
17.3 上下文
17.4 互模拟
17.5 确定性
17.6 CIL的规则与可靠性
17.6.1 上下文与应答器规则
17.6.2 派生规则与外部前提
17.7 概率签名方案
17.7.1 随机应答器
17.7.2 形式化证明
17.8 本章小结
参考文献
结束语
索引
参考文献
- ↑ 什么是时代的知识结构——汤胜天，搜狐，2016-11-04
- ↑ 陈丹青：何谓人文素质教育？ ，搜狐，2017-11-24