基于时序逻辑的安全协议验证方法的研究
发布时间：2021-04-15 08:24
安全协议是以密码学为基础的协议,它在因特网和分布式系统中提供各种各样的安全服务。近年来,利用形式化方法分析安全协议正在成为一个新的趋势。本文首先在分布式时序逻辑的基础上,给出了这个逻辑中局部公式的几组等价性定理并进行了证明,并和时序逻辑中的等价性公理进行了比较。然后用分布式时序逻辑描述了IEEE802.11i协议,给出了这个协议的事件结构模型,证明了三个主体之间的相互认证性。其次在分布式时序逻辑的基础上,增加了存在量词和全称量词,提出了分布式计算树时序逻辑。给出了分布式计算树时序逻辑的状态公式和路径公式的定义,以及这个逻辑的语义。同时也给出了分布式计算树时序逻辑中局部状态公式的几组等价性定理,并进行了证明。最后利用本文提出的分布式计算树时序逻辑描述了多方认证电子邮件协议,给出了这个协议的事件结构模型以及一些公平性公理。在有可信第三方参与和没有可信第三方参与的两种情况下,证明了发送者的不可否认性和接收者的不可否认性。
【文章来源】：南京航空航天大学江苏省 211工程院校
【文章页数】：79 页
【学位级别】：硕士
【文章目录】：
摘要
ABSTRACT
第一章 绪论
1.1 安全协议
1.2 安全协议的形式化方法
1.3 时序逻辑和分布式时序逻辑
1.4 本文的研究内容及结构安排
第二章 分布式时序逻辑
2.1 DTL 的语形
2.2 DTL 的语义
2.3 DTL 中公式的等价性定理
2.3.1 对偶律
2.3.2 幂等律
2.3.3 吸收律
2.3.4 分配律
2.3.5 扩张律
2.4 本章小结
第三章 用分布式时序逻辑验证IEEE802.11i 协议
3.1 IEEE802.11i 协议
3.2 IEEE802.11i 协议的DTL 模型
3.2.1 消息以及和消息有关的概念
3.2.2 基于信道的模型
3.2.3 DTL 的公理
3.2.3.1 K 公理以及由K 公理推出的公理
3.2.3.2 新鲜性和唯一性公理
3.2.3.3 关于信道CH 和主体的公理
3.2.3.4 关于公钥、私钥和共享密钥的公理
3.2.4 引理及命题
3.3 IEEE802.11i 协议的网络模型和事件结构模型
3.4 IEEE802.11i 协议的认证性
3.4.1 申请者认证
3.4.2 认证者认证
3.4.3 认证服务器认证
3.5 本章小结
第四章 分布式计算树时序逻辑
4.1 DCTL 的语形
4.2 DCTL 的语义
4.3 DCTL 中公式的等价性定理
4.3.1 对偶律
4.3.2 分配律
4.3.3 扩张律
4.4 本章小节
第五章 用分布式计算树时序逻辑分析多方认证电子邮件协议
5.1 多方认证电子邮件协议
5.2 多方认证电子邮件协议的网络模型
5.2.1 没有可信第三方的参与
5.2.2 有可信第三方的参与
5.3 用 DCTL 描述多方认证电子邮件协议
5.3.1 交换子协议的事件结构模型
5.3.2 取消子协议的事件结构模型
5.3.3 结束子协议的事件结构模型
5.4 多方认证电子邮件协议的不可否认性
5.4.1 发起者的不可否认性
5.4.1.1 没有可信第三方的参与
5.4.1.2 有可信第三方的参与
5.4.2 接收者的不可否认性
5.4.2.1 没有可信第三方的参与
5.4.2.2 有可信第三方的参与
5.5 本章小结
第六章 总结与展望
6.1 总结
6.2 展望
参考文献
致谢
在学期间研究成果及发表的学术论文
附录
【参考文献】：
期刊论文
[1]802.11i认证协议可验安全性形式化分析[J]. 宋宇波,胡爱群,姚冰心. 中国工程科学. 2010(01)
[2]Yahalom协议的分析及改进方案[J]. 陈春玲,赵艳春. 计算机应用与软件. 2008(07)
[3]IEEE 802.11i协议的形式化分析[J]. 吴开贵,徐成,廖振岚. 计算机应用. 2008(05)
[4]IEEE802.11i中四次握手过程的安全分析和改进[J]. 梁峰,史杏荣,曲阜平. 计算机工程. 2007(03)
[5]基于签密的多方认证邮件协议[J]. 王彩芬,贾爱库,刘军龙,于成尊. 电子学报. 2005(11)
[6]公平的多方不可否认协议[J]. 何冰,李肖坚,夏春和,夏克俭. 计算机工程与应用. 2005(27)
[7]电子商务协议中的可信第三方角色[J]. 卿斯汉. 软件学报. 2003(11)
[8]安全协议20年研究进展[J]. 卿斯汉. 软件学报. 2003(10)
[9]安全协议的设计与逻辑分析[J]. 卿斯汉. 软件学报. 2003(07)
[10]安全协议的形式化需求及验证[J]. 刘怡文,李伟琴. 计算机工程与应用. 2002(17)
本文编号：3138982
【文章来源】：南京航空航天大学江苏省 211工程院校
【文章页数】：79 页
【学位级别】：硕士
【文章目录】：
摘要
ABSTRACT
第一章 绪论
1.1 安全协议
1.2 安全协议的形式化方法
1.3 时序逻辑和分布式时序逻辑
1.4 本文的研究内容及结构安排
第二章 分布式时序逻辑
2.1 DTL 的语形
2.2 DTL 的语义
2.3 DTL 中公式的等价性定理
2.3.1 对偶律
2.3.2 幂等律
2.3.3 吸收律
2.3.4 分配律
2.3.5 扩张律
2.4 本章小结
第三章 用分布式时序逻辑验证IEEE802.11i 协议
3.1 IEEE802.11i 协议
3.2 IEEE802.11i 协议的DTL 模型
3.2.1 消息以及和消息有关的概念
3.2.2 基于信道的模型
3.2.3 DTL 的公理
3.2.3.1 K 公理以及由K 公理推出的公理
3.2.3.2 新鲜性和唯一性公理
3.2.3.3 关于信道CH 和主体的公理
3.2.3.4 关于公钥、私钥和共享密钥的公理
3.2.4 引理及命题
3.3 IEEE802.11i 协议的网络模型和事件结构模型
3.4 IEEE802.11i 协议的认证性
3.4.1 申请者认证
3.4.2 认证者认证
3.4.3 认证服务器认证
3.5 本章小结
第四章 分布式计算树时序逻辑
4.1 DCTL 的语形
4.2 DCTL 的语义
4.3 DCTL 中公式的等价性定理
4.3.1 对偶律
4.3.2 分配律
4.3.3 扩张律
4.4 本章小节
第五章 用分布式计算树时序逻辑分析多方认证电子邮件协议
5.1 多方认证电子邮件协议
5.2 多方认证电子邮件协议的网络模型
5.2.1 没有可信第三方的参与
5.2.2 有可信第三方的参与
5.3 用 DCTL 描述多方认证电子邮件协议
5.3.1 交换子协议的事件结构模型
5.3.2 取消子协议的事件结构模型
5.3.3 结束子协议的事件结构模型
5.4 多方认证电子邮件协议的不可否认性
5.4.1 发起者的不可否认性
5.4.1.1 没有可信第三方的参与
5.4.1.2 有可信第三方的参与
5.4.2 接收者的不可否认性
5.4.2.1 没有可信第三方的参与
5.4.2.2 有可信第三方的参与
5.5 本章小结
第六章 总结与展望
6.1 总结
6.2 展望
参考文献
致谢
在学期间研究成果及发表的学术论文
附录
【参考文献】：
期刊论文
[1]802.11i认证协议可验安全性形式化分析[J]. 宋宇波,胡爱群,姚冰心. 中国工程科学. 2010(01)
[2]Yahalom协议的分析及改进方案[J]. 陈春玲,赵艳春. 计算机应用与软件. 2008(07)
[3]IEEE 802.11i协议的形式化分析[J]. 吴开贵,徐成,廖振岚. 计算机应用. 2008(05)
[4]IEEE802.11i中四次握手过程的安全分析和改进[J]. 梁峰,史杏荣,曲阜平. 计算机工程. 2007(03)
[5]基于签密的多方认证邮件协议[J]. 王彩芬,贾爱库,刘军龙,于成尊. 电子学报. 2005(11)
[6]公平的多方不可否认协议[J]. 何冰,李肖坚,夏春和,夏克俭. 计算机工程与应用. 2005(27)
[7]电子商务协议中的可信第三方角色[J]. 卿斯汉. 软件学报. 2003(11)
[8]安全协议20年研究进展[J]. 卿斯汉. 软件学报. 2003(10)
[9]安全协议的设计与逻辑分析[J]. 卿斯汉. 软件学报. 2003(07)
[10]安全协议的形式化需求及验证[J]. 刘怡文,李伟琴. 计算机工程与应用. 2002(17)
本文编号：3138982
本文链接：https://www.wllwen.com/shekelunwen/ljx/3138982.html
