针对当前模型检测工具普遍不能检测带有异或运算安全协议的问题，提出了一个新的模型检测器SAT#。该模型检测器通过引入抽象异或项的概念及其运算规则，大大降低了攻击者生成的异或消息数量，解决了由于引入异或运算导致的状态空间爆炸问题。在此基础上，通过在SAT模型中增加基于抽象异或项的重写规则，扩展了攻击者的异或运算能力，实现了对带有异或运算安全协议的自动化检测。通过对BULL协议的检测，证明了抽象异或项的实用性，同时也证明了SAT#模型检测器的可靠性。
特别声明：本站注明稿件来源为其他媒体的文/图等稿件均为转载稿，本站转载出于非商业性的教育和科研之目的，并不意味着赞同其观点或证实其内容的真实性。如转载稿涉及版权等问题，请作者在两周内速来电或来函联系。
京公网安备 11040202430174号![京网文[2017]10376-1180号](/images/indexnew/www1024.jpg){kind=link}