Formal method-based analysis of the 5G Wireless Communication Protocol is crucial for identifying logical vulnerabilities and facilitating an all-encompassing security assessment, especially in the design phase. Natural Language Processing (NLP) assisted techniques and most of the tools are not widely adopted by the industry and research community. Traditional formal verification through a mathematics approach heavily relied on manual logical abstraction prone to being time-consuming, and error-prone. The reason that the NLP-assisted method did not apply in industrial research may be due to the ambiguity in the natural language of the protocol designs nature is controversial to the explicitness of formal verification. To address the challenge of adopting the formal methods in protocol designs, targeting (3GPP) protocols that are written in natural language, in this study, we propose a hybrid approach to streamline the analysis of protocols. We introduce a two-step pipeline that first uses NLP tools to construct data and then uses constructed data to extract identifiers and formal properties by using the NLP model. The identifiers and formal properties are further used for formal analysis. We implemented three models that take different dependencies between identifiers and formal properties as criteria. Our results of the optimal model reach valid accuracy of 39% for identifier extraction and 42% for formal properties predictions. Our work is proof of concept for an efficient procedure in performing formal analysis for largescale complicate specification and protocol analysis, especially for 5G and nextG communications.

翻译：基于形式化方法的5G无线通信协议分析对于识别逻辑漏洞、促进全方位安全评估（尤其在设计阶段）至关重要。自然语言处理（NLP）辅助技术及大多数工具尚未被工业界和研究界广泛采用。传统通过数学方法进行的形式化验证，很大程度上依赖人工逻辑抽象，这往往耗时且易错。NLP辅助方法未应用于工业研究的原因，可能在于协议设计自然语言的模糊性，与形式化验证所需的明确性存在根本矛盾。针对协议设计中采用形式化方法的挑战，本研究以自然语言编写的3GPP协议为目标，提出了一种混合方法来简化协议分析流程。我们引入了一个两阶段流水线：首先利用NLP工具构建数据，然后使用构建的数据通过NLP模型提取标识符和形式化属性。提取的标识符和形式化属性将进一步用于形式化分析。我们实现了三种模型，以标识符与形式化属性之间的不同依赖关系为标准。最优模型的结果显示：标识符提取的准确率为39%，形式化属性预测的准确率为42%。本工作验证了一种高效流程的概念可行性，可用于大规模复杂规范与协议分析（尤其针对5G及下一代通信）。