计算机工程与应用 ›› 2008, Vol. 44 ›› Issue (26): 95-98.DOI: 10.3778/j.issn.1002-8331.2008.26.029
张 超,韩继红,王亚弟,朱玉娜
ZHANG Chao,HAN Ji-hong,WANG Ya-di,ZHU Yu-na
摘要: 由于Blanchet安全协议一阶逻辑模型不能够给出易于理解的攻击序列,基于该安全协议一阶逻辑模型,对逻辑推理中的规则及合一化操作进行了分类,给出了操作置换规则,明确了改进系统中的一些关键性概念和命题。最后,以化简的Needham-Schroeder协议为例,对秘密性进行形式化验证,结果表明改进的系统能够给出易于理解的攻击序列。