摘要： 提出了采用模型检验方法对网络协议进行形式化分析及自动验证，建立了一个特定网络协议PAR的有限状态机模型，并用模型检验工具SMV验证其正确性，发现了该协议存在的一些缺陷。结果表明，利用符号模型检验方法分析检验网络协议是可行的。

关键词: 网络协议, 协议分析, 符号模型检验

Abstract: This paper proposes an new approach for formal analyzing and automatically verifing of network protocols. The protocol PAR is modeled as finite state machine, and analyzing in it’s vital aspects of properties. As a result, some limitations is finded in this protocol. This result shows that it is effective analyzing and checking the property of network protocols by symbol model checker.

Key words: Network protocols, Protocols analysis, Symbolic model checking