OAuth协议的形式化建模与验证

发布时间：2017-10-27 02:33

  本文关键词：OAuth协议的形式化建模与验证

  更多相关文章： 可满足性 OAuth协议 模型检验 ASLan++建模语言

【摘要】：过去的几年内,互联网日趋火热,各行各业的系统愈发需要与互联网进行融合,来优化自身系统架构,提升系统性能,进而创造更多的经济价值。同时,互联网内部的系统也迫切需要通过信息的共享以及信息的整合来达到强化系统并提供更好的服务的目的。为了实现信息的共享,2010年4月互联网工程任务组的OAuth工作组发布了OAuth1.0协议,规范了授权标准,提供了统一授权流程。通过OAuth,第三方应用可以访问用户授权的资源,而不需要用户提供其登录信息。OAuth定义了第三方应用和授权服务器以及用户之间的行为,通过规范不同角色的行为来实现信息的安全可靠共享。但是,如何保证不同角色在交互过程中,系统依旧能够提供安全可靠的服务呢?基于这个问题,本文采用了严格的数学方法——形式化方法,以最新版本OAuth 2.0协议中的授权码模型为实例,采用了ASLan++语言对授权协议进行了十分完善的形式化建模。ASLan++是AVANTSSAR平台的形式化建模语言,专门用来形式化描述建立在传输层和应用层上的对于安全十分敏感的组合Web服务的架构,并且规范化与这个架构相关联的安全策略和安全性质。本文在使用ASLan++语言建立的授权码形式化模型基础之上,从机密性,验证性,授权性,一致性,错误处理,令牌时效性六个方面进行模型分析,并通过线性时态逻辑公式表达这些性质,最后,采用AVANTSSAR的后台验证工具——SAT模型检查器,对这六个方面的性质进行自动化检查,最终找出了状态码、授权码的泄露以及用户授权存在不一致性等问题,针对这些问题,本文最后分析了出现这些问题的原因,并给予了解决方案。
【关键词】：可满足性 OAuth协议 模型检验 ASLan++建模语言
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP393.04
【目录】：

• 中文摘要6-7
• Abstract7-12
• 第一章 引言12-18
• 1.1 OAuth协议简介12-13
• 1.2 OAuth协议研究现状13-14
• 1.3 本文研究目标及贡献14-15
• 1.4 本文结构15-18
• 第二章 OAuth 2.0概述及授权码模型18-26
• 2.1 OAuth 2.0概述18-19
• 2.2 OAuth 2.0授权码模型架构及详细流程19-24
• 2.3 OAuth 2.0授权码模型实例24-25
• 2.4 本章小结25-26
• 第三章 AVANTSSAR形式化模型架构及语法规则26-32
• 3.1 AVANTSSAR形式化模型架构26-27
• 3.2 ASLan++语法规则27-31
• 3.3 AVANTSSAR后台验证工具31
• 3.4 本章小结31-32
• 第四章 建立OAuth 2.0授权码形式化模型32-46
• 4.1 搭建OAuth 2.0授权码形式化模型框架32-35
• 4.2 形式化描述OAuth.2.0授权码模型的用户登录阶段35-38
• 4.3 形式化描述OAuth 2.0授权码模型的授权码交换阶段38-39
• 4.4 形式化描述OAuth 2.0授权码模型的获取资源阶段39-41
• 4.5 形式化描述OAuth 2.0授权码模型的令牌更新阶段41-43
• 4.6 本章小结43-46
• 第五章 OAuth 2.0授权码模型性质分析与验证46-62
• 5.1 OAuth 2.0授权码模型性质分析46-48
• 5.2 对OAuth 2.0授权码模型性质进行建模48-57
• 5.3 OAuth 2.0授权码模型性质验证及结果分析57-60
• 5.4 本章小结60-62
• 第六章 总结及展望62-64
• 6.1 总结62-63
• 6.2 展望63-64
• 参考文献64-68
• 附录 授权码形式化模型源代码68-78
• 作者研究生阶段参加的项目及发表文章情况78-80
• 致谢80

【相似文献】

中国期刊全文数据库 前10条

1 余洁;李曦;周学海;高妍妍;;基于事件B的处理器形式化建模方法的研究[J];系统仿真学报;2007年03期

2 陈潇怡;何炎祥;;一种可扩展的数字权限表达语言的形式化建模及分析[J];武汉大学学报(理学版);2013年01期

3 马忠贵;叶斌;曾广平;涂序彦;;基于π演算的软件人群体形式化建模[J];北京理工大学学报;2006年02期

4 仲辉;陈超;王维平;李群;;基于π演算的指挥决策行为形式化建模研究[J];系统仿真学报;2007年15期

5 王世进;;分布式制造调度体系结构的π演算形式化建模[J];计算机工程与应用;2010年09期

6 陈伟芳;金智勇;高济;周斌斌;;MAS应用域本体的形式化建模及变换[J];浙江树人大学学报(自然科学版);2013年02期

7 丁湘陵;王志刚;;UML包与B结合的形式化建模研究[J];怀化学院学报;2010年11期

8 李月星;李晓娟;关永;王瑞;张杰;魏洪兴;;SpaceWire协议的形式化建模与概率分析[J];小型微型计算机系统;2013年09期

9 郝莉莉;杨惠珍;谢攀;;CPN在FCM形式化建模与验证中的应用[J];计算机仿真;2011年06期

10 沈啸;陈邦兴;唐晨;;基于Event-B的一种联锁逻辑的形式化建模研究[J];信息技术;2013年02期

中国重要会议论文全文数据库 前1条

1 蔡远利;于振华;王瑞峰;;多Agent系统形式化建模方法学[A];'2006系统仿真技术及其应用学术交流会论文集[C];2006年

中国博士学位论文全文数据库 前1条

1 胡晓辉;智能分布监控系统软件形式化建模和设计研究[D];西北工业大学;2007年

中国硕士学位论文全文数据库 前10条

1 夏倩倩;协同应用流程并行交互的形式化建模研究[D];内蒙古大学;2012年

2 肖知屹;列车安全距离控制形式化建模与验证[D];兰州交通大学;2014年

3 熊锡娇;列车自动防护系统的形式化建模与验证方法研究[D];华东师范大学;2012年

4 李丹;λ噬菌体生活周期的形式化建模与分析[D];上海交通大学;2007年

5 刘密霞;基于策略的信息安全模型及形式化建模的研究[D];兰州理工大学;2004年

6 周佳铭;基于PVS对SCADE开发轨交控制系统的形式化建模与验证[D];华东师范大学;2011年

7 濮阳;生物过程的形式化建模及仿真[D];上海交通大学;2007年

8 杨蒙;HMIPv6协议形式化建模及测试例生成方法研究[D];内蒙古大学;2010年

9 韩福荣;基于时间有色Petri网的联锁软件的形式化建模与分析[D];同济大学;2007年

10 严海星;OAuth协议的形式化建模与验证[D];华东师范大学;2015年

，

本文编号：1101594