面向多重协议组合实现的形式化安全检测理论和方法研究

Those attractive features of the future 5G network, such as “Super-Fast”, “Ultra-low Latency”, “Connections Anywhere”, “Full Opened Standards”, etc. drive the researches on 5G to be hot and require the future network divices should be implemented by those multiple-combined protocols from different network levels or different network domains. As a result, the security of multiple-combined protocol implementations are directly related to the security of 5G network devices. The security of the future 5G network devices can be achieved and studied by the security verifications of Multiple-Combined Protocol Implementations. In this project, we focus on such probem of multiple-combined protocol implementation security. We first extend the syntax and semantic definitions of Applied Pi Calculus to describe the protocol implementations in a formal, then we use the proposed syntax to define the proof system for the protocol implementation. Finially, the algorithms of automatic verification and the verification tools should be also proposed and experimented in this project.

未来5G网络的高速率、低延时、全兼容特性要求5G的网元设备必然为多重网络协议的组合实现。 5G网络的安全性将建立在这些实现着多种网络协议的网元设备的安全上。如何完成对这些多重协议组合实现(网元设备)的安全性检测将成为未来5G网络安全所要研究的重要课题。在本项目中，我们将从形式化安全分析的角度对多重协议组合实现的安全性检验理论和方法展开研究，通过提出针对多重协议组合实现的形式化描述方法，给出多重协议组合实现条件下不同强度的形式化安全性定义，给出完整的面向多重协议组合实现的安全演算证明理论和方法以及实现面向多重协议组合实现的自动安全检测算法和检测框架平台等研究目标，提出一种面向未来5G网元设备安全检验的形式化安全检验理论和方法。

本项目针对5G异构网络环境下多安全域交互并存，安全链路复杂、安全描述困难等问题，通过扩展形式化应用Pi演算方法和系统状态机方法，提出一种面向5G异构网络复杂系统安全的形式化安全验证方法。在研究中，我们首先围绕5G网络安全的特点进行研究，针对5G高带宽需求，提出了一种基于SDN架构的多信道并行传输方案并提供了安全保护方法；其次，针对5G网络海量IoT设备实时安全检测难题，提出了一种基于扩展FSM模型的自动化安全检测方法；最后，针对5G异构网络多信道、细粒度、动态通信的特点，提出了一种应用Pi演算的扩展模型，实现多信道安全模型的抽象描述。相关成果发表SCI收录论文5篇，会议论文5篇，申请国家发明专利4项。依托该项目部分研究成果，项目组已与国内知名通信公司取得合作，承担华为公司项目2项。