基于分段模型检测的云服务跨域认证协议的形式化分析与验证
Cloud Services Cross-domain Authentication Protocol Formal Analysis and Verification Based on Fragment Model Check作者机构:北京科技大学计算机与通信工程学院北京100083 铁道警察学院郑州450053 哈尔滨工业大学计算机学院哈尔滨150001
出 版 物:《计算机科学》 (Computer Science)
年 卷 期:2016年第43卷第4期
页 面:140-144页
学科分类:08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术(可授工学、理学学位)]
基 金:北京市科技计划项目(D141100003414002) "十二五"国家863高技术研究发展计划重大专项:亿级并发云服务器研制(2013AA01A209) 中央高校基本科研业务费项目(FRF-TP-14-042A2) 北京市自然科学基金(4142034) 北京市青年英才计划(YETP0380) 国家留学基金管理委员会资助
摘 要:针对多个云服务之间的跨域认证问题,提出一种基于SAML协议的云服务安全认证方案。阐明了该方案的关键技术机制,建立了云服务安全认证协议抽象模型;采用Casper和FDR软件的组合,通过模型检测法对云服务认证协议进行了形式化分析与验证;通过对安全认证协议进行分段模型检测,解决了安全协议形式化分析验证导致的状态空间爆炸问题。模型检测软件的实验结果验证了云服务跨域认证方案的有效性及安全性。