基于SAT的安全协议惰性形式化分析方法

提出了一种基于布尔可满足性问题的安全协议形式化分析方法 SAT-LMC,通过引入惰性分析的思想优化初始状态与转换规则,提高了安全性的检测效率。另一方面,通过在消息类型上定义偏序关系,SAT-LMC能够检测出更丰富的类型缺陷攻击。基于此方法实现了一个安全协议分析工具,针对Otway-Rees协议检测出了一种类型缺陷攻击;针对OAuth2.0协议,检测结果显示对现实中存在的一些应用场景,存在一种利用授权码截取的中间人攻击。

一种可检测类型缺陷攻击的SAT改进模型

针对现有SAT模型检测器不能检测类型缺陷攻击的问题,提出了一种新的SAT#改进模型.该模型通过在匹配模式下引入无类型变量,并利用无类型消息的概念,解除了SAT模型检测器对未知消息的类型限制,并且在诚实主体重写规则中用无类型消息替换了原来的强类型限制消息.通过增加消息匹配算法,使诚实主体能够接受带有类型缺陷的消息,从而实现类型缺陷攻击的检测.通过对Otway-Rees协议进行检测,不仅发现了已有的针对发起者A的类型缺陷攻击,而且发现了新的针对响应者B的类型缺陷攻击,其实验结果证明了SAT#模型具有一定的可靠性.

对Yahalom-Paulson协议的分析与改进

对原始Yahalom-Paulson协议和Backes与Pfitzmann的简化Yahalom-Paulson协议进行分析,指出各自协议中存在的漏洞.原始协议中存在类型缺陷攻击,简化协议中存在重放攻击导致协议参与实体间会话密钥不一致.对Yahalom-Paulson协议作出改进并使用串空间理论证明改进后协议的正确性.

安全协议类型漏洞攻击研究

类型漏洞攻击是对安全协议攻击的方法之一。当协议主体将所接收消息中的一种类型数据解释成其他类型数据时,就会发生类型漏洞攻击。该文描述了几种典型的类型漏洞攻击实例,结合实例指出了J.Heather等人提出的在消息中添加标识消息类型的附加信息以防止类型漏洞攻击的tag方法的局限性,并提出在协议实现中通过检测消息长度防止类型漏洞攻击的方法。

检测模型在安全协议分析中的应用

以认证测试方法为基础提出一种检测模型,通过对消息类型的检测和核对能够明确消息的初始产生主体,进而对主体的身份进行认证。将检测模型同认证测试方法相结合,能够克服原有认证测试方法缺乏判断消息初始产生者的缺点,从而在安全协议的分析中能够检测出协议可能存在的安全漏洞。通过对Neuman-Stubblebine协议的安全性验证表明,该方法能够有效地检测到原认证测试方法无法发现的类型攻击。

串空间模型中认证性测试方法的缺陷

指出了串空间模型中认证性测试方法存在的不足:1.分析认证性的过程中未考虑同一协议主体同时以不同身份参与协议运行的情况;2.分析认证性的过程中未考虑发生多轮协议同时运行的情况;3.认证性测试方法不能分析类型错误攻击。通过实例——Needham-Schroeder 协议分析了认证性测试方法存在不足的原因,并提出了改进方案。