基于SPIN的SSL3.0握手协议模型检测

文章介绍了密钥交换协议SSL3.0协议,并利用模型检测工具SPIN对其进行了形式化分析、建模和验证。实验结果表明此验证方法的正确性,证明了协议本身的安全性与可行性,并且提高了协议的验证效率。

基于串空间模型的SSL3.0协议认证性分析

形式化分析技术是揭示安全协议是否存在漏洞的重要途径,串空间模型是一种基于定理证明的、新兴的安全协议形式化模型。介绍了SSL3.0协议的握手过程和串空间模型的基本概念以及基于串空间模型的认证性测试方法,在此基础上建立了基于串空间的SSL协议握手过程的模型,并验证了SSL协议的认证性。

运用形式化语言N逻辑分析SSL3.0握手协议

近年来,人们在运用BAN逻辑进行形式化分析时,发现非形式化的理想化步骤是其致命缺陷,导致目前BAN逻辑的研究进展迟缓。有鉴于此,人们开始考虑采用另外一些形式化逻辑分析方法对协议的安全性进行分析。文章介绍了一种新的Nonmonotomic逻辑(简称N逻辑)的协议形式化分析方法,并运用此方法分析SSL3.0握手协议,对分析结果进行总结,提出协议的缺陷和逻辑本身需要进一步完善的地方。

用BAN逻辑方法分析SSL 3.0协议

形式化分析密码协议渐渐成为密码学中一个发展的新方向，因为形式化方法的确能检测出密码协议中的漏洞。ＢＡＮ逻辑是目前使用最广泛的。文章介绍了ＢＡＮ逻辑和ＳＳＬ３．０协议，并给出了用ＢＡＮ逻辑分析ＳＳＬ３．０协议的详细过程。

串空间模型及其认证测试方法的一种扩展与应用

认证测试方法是基于串空间模型的验证安全协议的一种形式化方法,由于串空间模型没有抽象更多的密码学原语,因此难以分析较复杂的安全协议。通过扩展消息项、子项关系以及入侵者模型,扩展了串空间模型及相应的认证测试方法。根据扩展后的认证测试方法,分析了SSL3.0握手协议,验证了该协议认证属性。