面向可信认证及授权协议的形式化建模与验证研究

《面向可信认证及授权协议的形式化建模与验证研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、命？料苓在汰大彥ＵｎｉｖｅｒｓｉｔｙｏｆＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙｏｆＣｈｉｎａ博士学位论文戀面向可信认鉦及援权切？仪的论文题目形式化建模与验证斫免注衫梅作者姓名学科专讨箅机应用故水业錢城导师姓名二〇—八年五月完成时间博士学位论文＿面向可信认证及授权协议的形式化建模与验证研究作者姓名：汪彩梅学科专业：计算机应用技术导师姓名：熊焰教授二〇一完成时间：八年五月二十曰ＵｎｉｖｅｒｓｉｔｙｏｆＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙｏｆ

2、Ｃｈｉｎａ’Ａｄｉｓｓｅｒｔａｔｉｏｎｆｏｒｄｏｃｔｏｒｓｄｅｇｒｅｅ義ＲｅｓｅａｒｃｈｏｎＦｏｒｍａｌＭｏｄｅｌｉｎａｎｄｇＶｅｒｉｆｉｃａｔｉｏｎｆｏｒＴｒｕｓｔｅｄＡｕｔｈｅｎｔｉｃａｔｉｏｎａｎｄＡｕｔｈｏｒｉｚａｔｉｏｎＰｒｏｔｏｃｏｌＡｕｔｈｏｒ：ＣａｉｍｅｉＷａｎｇＳｐｅｃｉａｌｉｔｙ：ＣｏｍｕｔｅｒＡｐｐｌｉｃａｔｉｏｎＴｅｃｈｎｏｌｏｐｇｙＳｕｐｅｒｖｉｓｏｒ：Ｐｒｏｆ．ＹａｎＸｉｏｎｇ’＂ＦｉｎｉｓｈｅｄＴｉｍｅ：Ｍａ２０２０１８ｙ，中国科学技

3、术大学学位论文原创性声明本人声明所呈交的学位论文，是本人在导师指导下进行研宄工作所取得的成果。除己特别加以标注和致谢的地方外，论文中不包含任何他人己经发表或撰写过的研究成果一。与我同工作的同志对本研宄所做的贡献均己在论文中作了明确的说明。作者签名：八初私签字日期：中国科学技术大学学位论文授权使用声明一作为申请学位的条件之，学位论文著作权拥有者授权中国科学技术大学拥有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅，可以将学位论文编入《中国学位论文全文数据库》等

4、有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。本人提交的电子文档的内容和纸质论文的内容相一致。保密的学位论文在解密后也遵守此规定。（）＾开□保密＿年作者签名：导师签名：，上＞＾，＾签字日期：签字日期：摘要摘要随着网络多样化发展，以及移动支付、社交网络等新技术的不断涌现，信息安全领域中的认证与授权技术得到了长足的发展。其中，可信认证协议及授权协议由于近几年广泛应用受到越来越多人的关注，这些协议具有安全属性多样性、逻辑结构复杂性等特点，使得构造验证模型与精确地刻画协议的安全属性变得

5、非常困难。因此有关可信认证协议及授权协议的安全性分析问题成了安全研宄中的一个难点和关键点。形式化验证是专门针对安全协议的安全性分析所提出一的种自动化检验方法，其原理是将安全协议转换为某种数学模型，将协议满足的安全要求转换为某种数学公式，然后通过验证建立的模型是否满足数学公式来检验安全协议的安全性。这种基于严谨的数学逻辑推导来达到证明效果的方法被公认为证明协议安全性的有效方法。针对上述问题，本文以可信属性认证系统、授权协议动态客户端注册协议的形式化建模与验证为研究重点，首先提出面向可选择披露的属性认证系统的形式化模型框架－Ｐｅ；其次

6、对复杂的可信属性认证协议Ｕｒｏｖ进行了形式化分析和安全性验证，。最后，论文对授权协议中的客户端动态注册协议进行了形式化建模在建模过程中发现了该协议在特定环境下具有安全隐患，随后对协议提出了改进措施，并通过形式化验证的方法对改进后的协议进行了安全性验证。具体研究内容如下：一１针对可信认证系统形式化建模的需求，提出了种面向可选择披露的属性认（）证系统的形式化模型框架。描述了可选择披露属性认证系统的抽象结构，刻画了系统中属性结构、实体结构和行为特征。对用户不同的属性添加了类型定义，给出分类函数及具体行为描述，对系统各个实体及实体之间的交

7、互行为进行抽象，其执行条件。针对系统需要满、具体的行为均给出了进程描述足的签名不可伪造性、匿名性和属性的隐私性给出安全特性定义。模型对于系统的设计与安全性分析具有实际意义。一２基于前Ｕ－Ｐ（）步工作，将模型检测方法应用于可信认证协议ｒｏｖｅ的形式化验一一－Ｐ－证中ｒｏｖｅ是，个嵌有属性的ＵＰｒｏｖｅ。Ｕ种新的复杂密码技术其核心是，用户通过该令牌可以实现身份的识别令牌，且不会泄露任何隐私信息。论－Ｐｒ文首先利用上述模型框架完成对Ｕｏｖｅ协议的形式化建模，以及协议满足－的有关安全属性的形式化建模ｉｆ工具完成了ＵＰ，然后通过ＰｒｏＶｅ

8、ｒｒｏｖｅ协议相关安