随着信息化时代的逐步推进，通信服务正发生着日新月异的变化。而网络协议作为构成通信服务骨架的关键部分，其安全性和可靠性是制约正常网络通信的因素。协议的漏洞及缺陷往往给攻击者提供了攻击可能性。为了对网络协议进行安全分析，为网络设备设计之初提供安全的保证，降低被攻击的风险，本文提出一种针对网络协议的形式化建模和基于模型检测技术的攻击发现方法。形式化方法与模型检测技术已经成为安全分析领域中的热门。本文针对网络协议应满足的安全属性，提出网络协议的形式化建模方法，并采用模型检测技术来验证这些安全属性。首先扩展CSP#语言及模型，从消息封装、线程广播、系统时钟和安全类库四个角度对模型进行扩展，实现对网络协议的形式化建模；建立网络协议的攻击者模型，确定攻击者掌握的知识集合及攻击行为；明确网络协议的安全目标，采用如线性时态逻辑等来表述网络协议要满足的安全属性；总结和归纳现有的攻击案例，构建网络协议的攻击模式库，进而生成模型中的攻击者进程，对网络协议作进一步安全分析；最后通过模型检测技术来验证安全属性的满足，继而发现网络协议存在的缺陷，提高应用此协议的网络产品的安全性。本文结合若干网络协议案例对该安全分析方法的流程做详细的说明，并对最终的实验结果进行综合分析和整体评价。根据本文的实验结果验证了该安全分析方法能够有效的检测中网络协议潜在的攻击，大大提高了网络协议开发的安全系数，继而能够保证整个网络环境的安全。