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