基于分段模型检测的云服务跨域认证协议的形式化分析与验证

发布时间：2018-05-19 12:07

  本文选题：云服务 + 认证协议　； 参考：《计算机科学》2016年04期

【摘要】：针对多个云服务之间的跨域认证问题,提出一种基于SAML协议的云服务安全认证方案。阐明了该方案的关键技术机制,建立了云服务安全认证协议抽象模型;采用Casper和FDR软件的组合,通过模型检测法对云服务认证协议进行了形式化分析与验证;通过对安全认证协议进行分段模型检测,解决了安全协议形式化分析验证导致的状态空间爆炸问题。模型检测软件的实验结果验证了云服务跨域认证方案的有效性及安全性。
[Abstract]:A secure authentication scheme for cloud services based on SAML protocol is proposed for cross-domain authentication of multiple cloud services. The key technical mechanism of the scheme is expounded, and the abstract model of cloud service security authentication protocol is established, and the formal analysis and verification of the cloud service authentication protocol are carried out by the combination of Casper and FDR software and the model checking method. The state space explosion caused by formal analysis and verification of security protocols is solved by segmented model checking of security authentication protocols. The experimental results of the model checking software verify the validity and security of the cross-domain authentication scheme for cloud services.
【作者单位】： 北京科技大学计算机与通信工程学院;铁道警察学院;哈尔滨工业大学计算机学院;
【基金】：北京市科技计划项目(D141100003414002) “十二五”国家863高技术研究发展计划重大专项:亿级并发云服务器研制(2013AA01A209) 中央高校基本科研业务费项目(FRF-TP-14-042A2) 北京市自然科学基金(4142034) 北京市青年英才计划(YETP0380) 国家留学基金管理委员会资助
【分类号】：TP393.08

【相似文献】

相关期刊论文 前10条

1 范红,冯登国;安全协议形式化分析方法综述之二——基于攻击结构性方法[J];网络安全技术与应用;2003年06期

2 郭宇燕;;安全协议的形式化分析方法初探[J];内江科技;2007年11期

3 范红,冯登国;一种混合的安全协议形式化分析技术[J];中国科学院研究生院学报;2002年03期

4 范红,冯登国,邹良惠;安全协议形式化分析方法综述之一:基于推理结构性方法[J];网络安全技术与应用;2003年05期

5 常亮;古天龙;;安全协议及其形式化分析研究[J];桂林电子工业学院学报;2006年04期

6 蔡永泉;朱勇;;一种改进的A(0)协议及其形式化分析[J];计算机工程与应用;2006年34期

7 亓文华;张其善;刘建伟;;关于安全协议的形式化分析方法的研究[J];遥测遥控;2007年02期

8 文静华;张梅;张焕国;;电子支付协议的博弈逻辑模型与形式化分析[J];微电子学与计算机;2007年09期

9 陆阳;肖军模;刘晶;;一种新的安全协议形式化分析方法——证据逻辑[J];计算机工程;2008年02期

10 卜奎昊;;安全协议形式化分析方法的融合性研究[J];西北师范大学学报(自然科学版);2010年05期

相关会议论文 前9条

1 文静华;张梅;张焕国;;电子支付协议的博弈逻辑模型与形式化分析[A];2007年全国开放式分布与并行计算机学术会议论文集(上册)[C];2007年

2 顾永跟;傅育熙;朱涵;吕银华;;基于进程演算的安全协议形式化分析[A];2005年全国理论计算机科学学术年会论文集[C];2005年

3 肖美华;邓宸芳;马小薏;薛锦云;江耘;;网络安全认证协议形式化分析[A];第二十次全国计算机安全学术交流会论文集[C];2005年

4 崔楠;汪学明;;基于SVO逻辑的电子商务协议非否认性形式化分析[A];逻辑学及其应用研究——第四届全国逻辑系统、智能科学与信息科学学术会议论文集[C];2008年

5 张梅;文静华;张焕国;;基于ATL的电子商务协议建模与形式化分析[A];2009年全国开放式分布与并行计算机学术会议论文集(上册)[C];2009年

6 李秋山;胡游君;;低成本RFID系统安全协议设计及其形式化分析[A];2006北京地区高校研究生学术交流会——通信与信息技术会议论文集（上）[C];2006年

7 谢鸿波;周明天;;安全协议的形式化技术:述评[A];’2004计算机应用技术交流会议论文集[C];2004年

8 徐锐;;设计安全协议[A];第十八次全国计算机安全学术交流会论文集[C];2003年

9 刘忠;王成道;;基于汉语语意形式系统的符号化研究[A];第六届全国计算机应用联合学术会议论文集[C];2002年

相关博士学位论文 前10条

1 范红;安全协议形式化分析理论与方法[D];中国人民解放军信息工程大学;2003年

2 张帆;无线网络安全协议的形式化分析方法[D];西安电子科技大学;2007年

3 陈俊清;可信普适服务的形式化分析与验证[D];上海交通大学;2012年

4 汪学明;多方安全协议的形式化分析方法研究与应用[D];贵州大学;2008年

5 杨超;无线网络协议的形式化分析与设计[D];西安电子科技大学;2008年

6 鲁来凤;安全协议形式化分析理论与应用研究[D];西安电子科技大学;2012年

7 朱薏;数据库管理系统安全性形式化分析研究[D];华中科技大学;2014年

8 赵辉;安全协议形式化分析技术的研究[D];大连理工大学;2010年

9 何安平;基于层次模型的混合系统形式化分析与验证[D];兰州大学;2011年

10 李云峰;电子商务协议安全性的形式化分析方法研究[D];西南交通大学;2009年

相关硕士学位论文 前10条

1 张玲玲;物联网安全协议形式化分析与验证[D];聊城大学;2015年

2 王洁;公平不可否认协议设计及其形式化分析[D];重庆大学;2008年

3 成敏盈;电力系统安全协议形式化分析技术研究[D];广东工业大学;2008年

4 李轶，

本文编号：1910035