一种可检测类型缺陷攻击的SAT改进模型
杨元原
马文平
刘维博
白晓峰
1.西安电子科技大学计算机网络与信息安全教育部重点实验室,西安,7100712.西安电子科技大学计算机网络与信息安全教育部重点实验室,西安,7100713.西安电子科技大学计算机网络与信息安全教育部重点实验室,西安,7100714.西安电子科技大学计算机网络与信息安全教育部重点实验室,西安,710071
摘要：针对现有SAT模型检测器不能检测类型缺陷攻击的问题，提出了一种新的SAT#改进模型．该模型通过在匹配模式下引入无类型变量，并利用无类型消息的概念，解除了SAT模型检测器对未知消息的类型限制，并且在诚实主体重写规则中用无类型消息替换了原来的强类型限制消息．通过增加消息匹配算法，使诚实主体能够接受带有类型缺陷的消息，从而实现类型缺陷攻击的检测．通过对Otway—Rees协议进行检测，不仅发现了已有的针对发起者A的类型缺陷攻击，而且发现了新的针对响应者B的类型缺陷攻击，其实验结果证明了SAT#模型具有一定的可靠性．
关键词：安全协议形式化分析模型检测重写规则类型缺陷攻击匹配模式图形编码满足性问题
分类号：TP393(计算技术、计算机技术)
资助基金：国家高技术研究发展计划（863计划）(2007AA012472)国家自然科学基金(60773002)高等学校学科创新引智计划计划)(B08038)高等学校博士学科点专项科研基金(20100203110003)
论文发表日期：2011-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
英文信息