改进的安全协议一阶逻辑模型  

Improved first-order logic model for security protocols

作　　者：张超[1] 韩继红[1] 王亚弟[1] 朱玉娜[1] 

机构地区：[1]信息工程大学电子技术学院,郑州450004

出　　处：《计算机工程与应用》2008年第26期95-98,101,共5页Computer Engineering and Applications

摘　　要：由于Blanchet安全协议一阶逻辑模型不能够给出易于理解的攻击序列,基于该安全协议一阶逻辑模型,对逻辑推理中的规则及合一化操作进行了分类,给出了操作置换规则,明确了改进系统中的一些关键性概念和命题。最后,以化简的Needham-Schroeder协议为例,对秘密性进行形式化验证,结果表明改进的系统能够给出易于理解的攻击序列。The previous Blanchet first-order logic model for security protocols can not give the common attack sequence.An improved model is introduced to solve this problem.Compared with the Blanchet model,the new model classifies the rules and unify operations,gives operation replacement rules and definitizes some key related concepts and propositions in the improved system.Finally,the example by the simplified Needham-Schroeder protocol shows the improved system can give a common attack sequence.

关 键 词：安全协议 形式化分析 一阶逻辑模型 攻击序列重构 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]