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

来源 :计算机科学 | 被引量 : 1次 | 上传用户:MyFairy83
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
针对多个云服务之间的跨域认证问题,提出一种基于SAML协议的云服务安全认证方案。阐明了该方案的关键技术机制,建立了云服务安全认证协议抽象模型;采用Casper和FDR软件的组合,通过模型检测法对云服务认证协议进行了形式化分析与验证;通过对安全认证协议进行分段模型检测,解决了安全协议形式化分析验证导致的状态空间爆炸问题。模型检测软件的实验结果验证了云服务跨域认证方案的有效性及安全性。
其他文献
主要讨论了测量失真度的准同步方法--采样周期不要求与信号周期严格同步.该方法用于失真度测量,有效地克服了传统的基于DFT的失真度测量方法中非整周期采样引起的频谱泄漏对
主要探讨了如何在DSPs上高效地实现MPEG-4的视频压缩算法,问题的视频对象的数据结构并有效利用DSPs甚长指令和流水线的特点以加速压缩过程的实现.此外,还利用了混合编成的方
线路故障后快速寻找故障点为保证电网安全稳定运行的一项关键技术,也是长期以来困扰电网运行的世界性技术难题之一。1997年初,中国电力科学研究院与辽宁省电力有限公司开始精诚
在简单介绍动态K值加权室内定位算法(EWKNN)并分析其不足的基础上,探索研究了基于动态K值及AP MAC地址筛选的室内定位算法。该算法首先使用EWKNN方法动态选择参考点个数,并根据
节点或边不可靠网络的可靠度分析问题是NP-hard问题,网络节点和边都不可靠的假设更接近现实。基于网络节点和边二元状态的假设,构建了节点和边不可靠网络的形式化模型,给出了分析节点和边不可靠网络可靠度的NEF_MDD算法。该算法将单个节点与其未访问邻接边划分为一个集合,通过枚举节点和边的不同组合,合并导致子网同构的冗余状态,获得简化后的状态向量和可靠度向量,并用一个多值决策图变量来表述。通过使用自定