# From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis

arXiv: https://arxiv.org/abs/2308.03277 · HTML: https://mlsanity.com/paper/2308.03277/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 31 references that are in the map.
- First posted on arXiv 7 Aug 2023.

## Builds on (most cited first, 13 of 13)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Pre-train, Prompt, and Predict: A Systematic Survey of Prompting Methods in Natural Language Processing](https://mlsanity.com/paper/2107.13586/) (2021)
- [A Formal Analysis of 5G Authentication](https://mlsanity.com/paper/1806.10360/) (2018)
- [CyNER: A Python Library for Cybersecurity Named Entity Recognition](https://mlsanity.com/paper/2204.05754/) (2022)
- [Knowledge Graph Anchored Information-Extraction for Domain-Specific Insights](https://mlsanity.com/paper/2104.08936/) (2021)
- [Tabula: A Language to Model Spreadsheet Tables](https://mlsanity.com/paper/1707.02833/) (2017)
- [Radar Altimeter Redesign for Multi-Stage Interference Risk Mitigation in 5G and Beyond](https://mlsanity.com/paper/2305.05579/) (2023)
- [Formal and Fuzzing Amplification: Targeting Vulnerability Detection in 5G and Beyond](https://mlsanity.com/paper/2307.05758/) (2023)
- [Formal-Guided Fuzz Testing: Targeting Security Assurance from Specification to Implementation for 5G and Beyond](https://mlsanity.com/paper/2307.11247/) (2023)
- [NLP-based Cross-Layer 5G Vulnerabilities Detection via Fuzzing Generated Run-Time Profiling](https://mlsanity.com/paper/2305.08226/) (2023)
- [Information Extraction in Domain and Generic Documents: Findings from Heuristic-based and Data-driven Approaches](https://mlsanity.com/paper/2307.00130/) (2023)
- [Distributed 3D-Beam Reforming for Hovering-Tolerant UAVs Communication over Coexistence: A Deep-Q Learning for Intelligent Space-Air-Ground Integrated Networks](https://mlsanity.com/paper/2307.09325/) (2023)

## Built on by (most cited first, 1 of 1)

- [Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach](https://mlsanity.com/paper/2312.17353/) (2023)

## Abstract (arXiv)

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.