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

An improved SAT model for detection of type flaw attacks

作　　者：杨元原[1] 马文平[1] 刘维博[1] 白晓峰[1] 

机构地区：[1]西安电子科技大学计算机网络与信息安全教育部重点实验室,西安710071

出　　处：《沈阳工业大学学报》2011年第4期422-427,共6页Journal of Shenyang University of Technology

基　　金：国家863计划资助项目(2007AA01Z472);国家自然科学基金资助项目(60773002);高等学校创新引智计划资助项目(B08038);高等学校博士学科点专项科研基金资助项目(20100203110003)

摘　　要：针对现有SAT模型检测器不能检测类型缺陷攻击的问题,提出了一种新的SAT#改进模型.该模型通过在匹配模式下引入无类型变量,并利用无类型消息的概念,解除了SAT模型检测器对未知消息的类型限制,并且在诚实主体重写规则中用无类型消息替换了原来的强类型限制消息.通过增加消息匹配算法,使诚实主体能够接受带有类型缺陷的消息,从而实现类型缺陷攻击的检测.通过对Otway-Rees协议进行检测,不仅发现了已有的针对发起者A的类型缺陷攻击,而且发现了新的针对响应者B的类型缺陷攻击,其实验结果证明了SAT#模型具有一定的可靠性.For the problem that the current SAT model checker can not detect type flaw attacks, a new improved model SAT#was proposed. Through introducing non-type variables under the match mode and defining the concept of non-type messages, the new model relieves the type restriction of SAT model checker to unknown messages. Moreover, it replaces the original strong type restriction messages with the non-type messages in the rewrite rules of veracity agent. Through adding the message match algorithm, the veracity agent can accept the type flaw messages to realize the detection of type flaw attacks. The detection results on Otway-Rees protocol demonstrate that not only the existing type flaw attack to the initiator A but also a new type flaw attack to the responder B are found. The experimental results show that the SAT# model has a certain reliability.

关 键 词：安全协议 形式化分析 模型检测 重写规则 类型缺陷攻击 匹配模式 图形编码 满足性问题 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]