关键词: 安全协议, 模型检测, 简单进程元语言解释器, 状态爆炸

Abstract: Aiming at a more efficient analysis and verification of the security protocol with the model checking technology，this paper proposes a more efficient modeling algorithm with a wider applicability and higher level of automation.Based on this modeling algorithm，the“Generative System of Network Security Protocol Verification Model” is developed.This system can efficiently analyze and verify the security protocol.During the modeling of the intruder，the system improves the efficiency of verification and solves the problem of state explosion by using such optimization strategies as the partial order reduction，syntax reordering and type checking.

Key words: security protocol, model checking, Simple PROMELA Interpreter（SPIN）, state explosion