一种可检测类型缺陷攻击的SAT改进模型

• 作者: 刘维博 杨元原 白晓峰 马文平
• 来源期刊: 沈阳工业大学学报
• 学科: 工学
• 关键词: 安全协议 形式化分析 模型检测 重写规则 类型缺陷攻击 匹配模式 图形编码 满足性问题
• 年，卷（期）: 2011,（4）
• 所属期刊栏目: 信息科学与工程
• 页码范围: 422-427
• 页数: 6页
• 分类号: TP393
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	马文平		79	449	10.0	17.0
2	白晓峰		3	15	1.0	3.0
3	杨元原		6	25	3.0	5.0
4	刘维博		4	8	2.0	2.0