Abstract: 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.

Key words: security protocols, formal analysis, first-order logic model, reconstruction of attack sequence

摘要： 由于Blanchet安全协议一阶逻辑模型不能够给出易于理解的攻击序列，基于该安全协议一阶逻辑模型，对逻辑推理中的规则及合一化操作进行了分类，给出了操作置换规则，明确了改进系统中的一些关键性概念和命题。最后，以化简的Needham-Schroeder协议为例，对秘密性进行形式化验证，结果表明改进的系统能够给出易于理解的攻击序列。

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