物联网技术的发展与5G时代的降临伴生出了各式各样的网络服务需求,为特定的网络服务场景设计专用的网络协议这一有效方法也将协议工程推向了相关研发人员的视野中。然而,网络协议的设计总是需要考虑其功能的正确性、鲁棒性以及在网络环境中抵抗恶意攻击的能力。在形式化验证技术蓬勃发展、算力日渐增强的今天,这些协议设计时的顾虑被逐步抽象和归纳为形式化模型上的功能安全性质与信息安全性质,但这种模型抽象本身仍是一个较为困难的任务。即便在过去的几十年中有许多的网络协议建模和分析方法被提出,但其中的大多数工作都迫使了将功能安全性质与信息安全性质拆分在不同的模型上处理,而没有直接考虑两者的关联,因此仍存在模型等价性和潜在冲突等问题。近几年虽然已经有一些工作致力于协同建模和分析,但这些工作主要适用于特定的工业控制或信息物理融合系统,在应用于结构多变且异质化的通用网络协议时仍表现得不够理想。在充分调研和理解国内外相关的形式验证及协同建模工作的基础上,结合网络协议普适的分布式、可配置、信息交换等特征,本文针对通用网络协议的功能安全与信息安全性特点,提出了一种协同建模与分析的方法,以构建完整的协议建模、性质规约及分析的方法论,并借助实现工具进行了案例分析。具体地,本文的主要贡献如下:1.设计了一种适用于通用网络协议的功能安全与信息安全要素协同建模框架,该框架可以细分为协议元模板构建、协议行为建模和协议架构建模三个部分,并基于此给出了几类功能安全和信息安全性质规约方法。其中,协议元模板构建包括对协议运行过程中涉及的结构化数据类型、协议中的抽象进程及其属性和通信端口、协议进程所处的抽象环境及其属性和逻辑信道、协议中各进程及攻击者的初始知识、协议中的函数之间的公理关系等的描述。协议行为建模引入进程图状态机及其上的各类操作步来对进程的消息打包、抽取、密码学操作、通信操作等进行细致的刻画。协议架构建模引入例化拓扑图模型,并通过其上的进程实例、环境实例以及两者之间的拓扑连线来对协议中的实际执行的进程以及相应的属性参数、通信关系等进行刻画。2.基于前述的统一语义建模框架设计了一套模型转换方法。首先在对UPPAAL模型检测工具和ProVerif安全协议验证工具的项目结构进行充分调研的基础上分别构建了一套语法对齐模型,能够将两者的模型进行结构化表达。然后将统一语义建模框架中的各类建模元素分别映射到两类语法对齐模型上,从而实现从统一语义模型向UPPAAL和ProVerif模型的语义化翻译。3.基于本文的建模和转换方法论采用C#语言和Avalonia框架实现了一套全流程工具,能够跨平台地运行图形化建模和向UPPAAL和ProVerif的转换功能。我们还以该实现工具结合5G-AKA网络协议的初始化过程给出了案例研究和分析,比对了翻译前后的模型以及验证结果,支撑了本文的方法论及实现工具的有效性。综上,本文通过设计一套面向通用网络安全协议的统一语义模型,对其功能安全与信息安全要素协同建模,并转换到UPPAAL和ProVerif形式化验证工具上进行功能安全性质与信息安全性质的验证,借助实现工具对5G-AKA协议初始化过程展开案例分析,最终分析结果符合预期,证实了本文工作的有效性。