摘要
针对当前模型检测工具普遍不能检测带有异或运算安全协议的问题,提出了一个新的模型检测器SAT#.该模型检测器通过引入抽象异或项的概念及其运算规则,大大降低了攻击者生成的异或消息数量,解决了由于引入传统异或运算导致的状态空间爆炸问题.在此基础上,通过在SAT模型中增加基于抽象异或项的重写规则,扩展了攻击者的异或运算能力,实现了对带有异或运算安全协议的自动化检测.通过对BULL协议的检测,证明了抽象异或项的实用性,同时也证明了SAT#模型检测器的可靠性.
Since most of the current model checking tools can not detect security protocols with XOR, a new model checker named SAT# is proposed. By defining the concept of abstract XOR term and its reduction rules, the new model greatly reduces the number of XOR messages produced by the intruder, and resolves the state space explosion problem resulting from the introduction of XOR operations, on the basis of which by adding the rewrite rules of XOR based on the abstract XOR term, the new model endows the intruder with the XOR operations, and thus is able to automatically detect the security protocols with XOR. The detection results of the BULL protocol show not only the practicality of the abstract XOR term but also the reliability of the SAT# .
出处
《西安电子科技大学学报》
EI
CAS
CSCD
北大核心
2012年第4期120-125,183,共7页
Journal of Xidian University
基金
国家自然科学基金资助项目(61072140)
高等学校创新引智计划资助项目(B08038)
高等学校博士学科点专项科研基金资助项目(20100203110003)
陕西省教育厅科研计划资助项目(2010JK825)
关键词
安全协议
形式化分析
模型检测
代数性质
security protocols
formal analyses
model checking
algebraic properties
