安全协议一阶逻辑模型中攻击重构的实现

Implementation of Attack Reconstruction in First-order Logic Model for Security Protocols

针对安全协议一阶逻辑模型不能够给出易于理解的攻击序列的问题,对安全协议一阶逻辑模型进行扩展,对逻辑推理中的规则及合一化操作进行分类,给出操作置换规则,在此基础上开发能对攻击进行重构的协议验证原型系统。通过具体的应用例子对其秘密性进行形式化验证,结果表明系统能给出易于理解的攻击序列。

According to the problem that first-order logic model for security protocols can not give the understandable attack sequence, this paper introduces an improved model, which classifies the rules and unify operations, presents operation replacement rules, and develops a new system that can reconstruct attack sequence. Example with the simplified Needham-Schroeder protocol shows the effectiveness of the system.