论文部分内容阅读
针对现有SAT模型检测器不能检测类型缺陷攻击的问题，提出了一种新的SAT#改进模型．该模型通过在匹配模式下引入无类型变量，并利用无类型消息的概念，解除了SAT模型检测器对未知消息的类型限制，并且在诚实主体重写规则中用无类型消息替换了原来的强类型限制消息．通过增加消息匹配算法，使诚实主体能够接受带有类型缺陷的消息，从而实现类型缺陷攻击的检测．通过对Otway—Rees协议进行检测，不仅发现了已有的针对发起者A的类型缺陷攻击，而且发现了新的针对响应者B的类型缺陷攻击，其实验结果证明了SAT#模型具有一定的可靠