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

作者：杨元原; 马文平; 刘维博; 俞优; 顾健

来源：西安电子科技大学学报, 2012, (04): 120-125+183.

• 安全协议
• 形式化分析
• 模型检测
• 代数性质 security protocols
• formal analyses
• model checking
• algebraic properties

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

• 出版日期2012
• 单位西安电子科技大学; 公安部第三研究所