带有异或运算安全协议的自动化检测

针对当前模型检测工具普遍不能检测带有异或运算安全协议的问题,提出了一个新的模型检测器SAT#.该模型检测器通过引入抽象异或项的概念及其运算规则,大大降低了攻击者生成的异或消息数量,解决了由于引入传统异或运算导致的状态空间爆炸问题.在此基础上,通过在SAT模型中增加基于抽象异或项的重写规则,扩展了攻击者的异或运算能力,实现了对带有异或运算安全协议的自动化检测.通过对BULL协议的检测,证明了抽象异或项的实用性,同时也证明了SAT#模型检测器的可靠性.

Automatic detection of security protocols with XOR

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#.