以LTE技术为代表的4G移动通信技术已经深入人们的工作和生活中,其安全问题日益被人们所关注。LTE系统中移动网络协议的安全缺陷具有隐蔽性强、易被利用、影响范围广等特点,常被不法分子所利用来达到破坏LTE系统安全的目的。而LTE系统与之前的移动通信系统相比,在架构上做出了革命性的变革,各个功能实体所完成的功能任务重新被划分,系统中使用的网络协议和协议所实现的功能都做出了较大调整。这给我们的研究工作带来了新的挑战与难度。因此,本文运用形式化分析方法中的模型检测方法对LTE系统移动网络协议的安全性进行分析与研究,主要研究内容如下:首先,为了解决模型检测方法状态空间爆炸的难题,本文先利用攻击树模型分析方法和安全要素分析方法对LTE网络协议进行初步的安全性分析,在得到初步的攻击序列后再对攻击序列进行可行性分析,然后深入分析可行性最高的攻击序列对应的协议流程的安全缺陷,得到了接入过程和切换过程中可能存在的安全缺陷。分析结果能够帮助我们更有效地定位可能存在安全缺陷的协议流程。然后,在对有色Petri网及其分析方法和工具充分研究的基础上,利用有色Petri网对可能存在安全缺陷的协议流程进行建模,通过有色Petri网的逆向状态分析方法和有色Petri网的辅助分析工具分析验证了相关协议流程的安全缺陷。