运用SPIN对开放授权协议OAuth 2.0的分析与验证

发布时间：2018-11-22 19:22

【摘要】：OAuth 2.0协议是一种开放授权协议,主要用于解决用户账号关联与资源共享问题。但是,其弱安全性导致各网络公司海量用户信息泄露,且OAuth 2.0传输数据采用的https通道效率低下,成为黑客攻击对象。提出采用http通道传输OAuth 2.0协议数据,基于Promale语言及Dolev-Yao攻击者模型对OAuth 2.0协议建模,运用SPIN进行模型检测。形式化分析结果表明,采用公钥加密体系对OAuth 2.0协议进行加密不安全。上述建模方法对类似的授权协议形式化分析有重要借鉴意义。
[Abstract]:OAuth 2.0 protocol is an open authorization protocol, which is mainly used to solve the problem of user account association and resource sharing. However, its weak security results in massive information leakage of users in various network companies, and the https channel used in OAuth 2.0 data transmission is inefficient, so it becomes the target of hacker attack. In this paper, http channel is used to transmit OAuth 2.0 protocol data. Based on Promale language and Dolev-Yao attacker model, OAuth 2.0 protocol is modeled, and SPIN is used for model checking. The results of formal analysis show that using public key encryption system to encrypt OAuth 2.0 protocol is not secure. The above modeling methods can be used for reference for formal analysis of similar authorization protocols.
【作者单位】： 华东交通大学软件学院;
【基金】：国家自然科学基金资助项目(61163005) 计算机软件新技术国家重点实验室开放课题资助项目(KFKT2012B18) 江西省自然科学基金资助项目(20132BAB201033) 江西省高校科技落地计划项目(KJLD13038) 江西省对外科技合作技术资助项目(20151BDH80005) 华东交通大学研究生创新计划资助项目(YC2014-X007)
【分类号】：TP393.08

【参考文献】

相关期刊论文 前5条

1 杨元原;马文平;刘维博;;模型检测中可变攻击者模型的构造[J];北京邮电大学学报;2011年02期

2 李兴锋;张新常;杨美红;阎保平;;基于SPIN的模块化模型检测方法研究[J];电子与信息学报;2011年04期

3 XIAO Meihua;MA Chenglin;DENG Chunyan;ZHU Ke;;A Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic[J];Chinese Journal of Electronics;2015年01期

4 胡良文;马金晶;孙博;;基于Spin的SysML活动图验证框架[J];计算机科学与探索;2014年07期

5 余鹏;魏欧;韩兰胜;牛耘;;模型检测网络传播干预策略[J];计算机科学与探索;2014年08期

【共引文献】

相关期刊论文 前7条

1 高洪博;李清宝;王炜;朱瑜;;基于敏感位置识别的状态化简技术研究[J];电子与信息学报;2013年03期

2 钱成;燕雪峰;周勇;徐海生;;基于状态约简的顺序图和状态图一致性检测[J];计算机应用研究;2014年05期

3 贺志宏;曾庆凯;;基于SPIN的LTL属性分解方法研究[J];计算机应用与软件;2014年07期

4 肖美华;程道雷;胡磊;;基于Spin/Promela的Woo-Lam协议安全性质高效验证[J];计算机与数字工程;2014年10期

5 肖美华;朱科;马成林;;基于SPIN的Andrew Secure RPC协议并行攻击模型检测[J];计算机科学;2015年07期

6 顾名宇;;数理逻辑的程序可靠性验证[J];山东农业大学学报(自然科学版);2015年04期

7 王曦;徐中伟;;基于启发式NDFS的模型检测新算法[J];小型微型计算机系统;2012年08期

相关博士学位论文 前3条

1 包力;Web服务组合形式化建模与验证研究[D];大连海事大学;2009年

2 林英;多核软件形式化建模、验证及性能评价方法研究[D];云南大学;2013年

3 高洪博;指令诱发型硬件木马检测技术研究[D];解放军信息工程大学;2013年

相关硕士学位论文 前10条

1 程莹;网络安全协议的模型检测分析及验证系统[D];南昌大学;2010年

2 吕审;NuSMV模型检测的研究及应用[D];武汉理工大学;2011年

3 李静;网络安全认证协议自动分析系统[D];南昌大学;2007年

4 王兵;电子商务协议的形式化分析[D];南昌大学;2007年

5 魏小勇;符号模型检测的研究[D];西安理工大学;2008年

6 刘俏威;SPIN模型检测的形式化分析机理研究及应用[D];南昌大学;2008年

7 熊昊;模型检测形式化分析中若干关键问题研究[D];南昌大学;2008年

8 王胜;基于SystemC的时态逻辑属性验证方法研究[D];北京化工大学;2009年

9 舒良春;基于SPIN/Promela的UML模型验证工具设计与实现[D];南昌大学;2009年

10 安鑫;面向一类基于轮数的分布式算法的状态空间分析与模型检测[D];山东大学;2010年

【二级参考文献】

相关期刊论文 前10条

1 邱慧敏;杨义先;钮心忻;;无线传感器网络中广播通信的安全协议设计[J];北京邮电大学学报;2006年05期

2 杜杰;江国华;;基于模型检测的UML状态图和顺序图一致性检测[J];电子科技;2012年02期

3 高晓星;李晓霞;薛冰;;基于UML和SPIN的软件安全模型验证[J];长沙大学学报;2013年05期

4 颜志军,孙宝文,王天梅;基于UML的业务流程模型分析方法研究[J];计算机工程与应用;2004年29期

5 周春燕;李绪蓉;周良;;UML活动图模型正确性诊断方法[J];计算机工程;2011年14期

6 吴翔虎;曲明成;李建中;王志超;;活动图并发语义代码自动生成算法设计[J];哈尔滨工业大学学报;2012年09期

7 王松锋;熊选东;付建丹;张亮忠;;基于Petri网的SysML活动图的分析与验证[J];计算机科学;2012年09期

8 刘军霞;熊选东;王松锋;;基于随机Petri网的SysML状态机图的验证[J];计算机应用与软件;2013年06期

9 张筠;崔哲;张宇渊;;UML和Petri网的建模验证方法[J];火力与指挥控制;2013年10期

10 魏欧;袁泳;蔡昕烨;黄志球;徐丙凤1;;循环对称化简及在三值模型上的扩展[J];软件学报;2011年06期

相关博士学位论文 前1条

1 韩兰胜;计算机病毒的传播模型及其求源问题研究[D];华中科技大学;2006年

相关硕士学位论文 前3条

1 单卓为;基于SPIN的UML模型验证技术的研究[D];西北大学;2008年

2 薛克;基于SPIN的UML活动图验证[D];华东师范大学;2008年

3 张冠女;基于rCOS的SysML形式化研究[D];内蒙古大学;2008年

，

本文编号：2350299