排序方式： 共有3条查询结果，搜索用时 2 毫秒
1
1.
针对当前模型检测工具普遍不能检测带有异或运算安全协议的问题,提出了一个新的模型检测器SAT#.该模型检测器通过引入抽象异或项的概念及其运算规则,大大降低了攻击者生成的异或消息数量,解决了由于引入传统异或运算导致的状态空间爆炸问题.在此基础上,通过在SAT模型中增加基于抽象异或项的重写规则,扩展了攻击者的异或运算能力,实现了对带有异或运算安全协议的自动化检测.通过对BULL协议的检测,证明了抽象异或项的实用性,同时也证明了SAT#模型检测器的可靠性. 相似文献
2.
提出了一个可变攻击者模型构造方案. 该方案通过定义抽象项的概念及其运算规则,大大降低了攻击者进行代数运算的复杂度. 定义了攻击者行为库和攻击规则选择算法,使检测者能根据不同的协议构造不同的攻击者模型. 由于攻击者行为可任意组合,故实现了攻击者模型的可变性. 可变攻击者模型保证了模型检测工具对协议分析的效率和准确性. 相似文献
3.
针对现有SAT模型检测器不能检测类型缺陷攻击的问题,提出了一种新的SAT#改进模型.该模型通过在匹配模式下引入无类型变量,并利用无类型消息的概念,解除了SAT模型检测器对未知消息的类型限制,并且在诚实主体重写规则中用无类型消息替换了原来的强类型限制消息.通过增加消息匹配算法,使诚实主体能够接受带有类型缺陷的消息,从而实现类型缺陷攻击的检测.通过对Otway Rees协议进行检测,不仅发现了已有的针对发起者A的类型缺陷攻击,而且发现了新的针对响应者B的类型缺陷攻击,其实验结果证明了SAT#模型具有一定的可靠性. 相似文献
1