Trustworthy Formal Verification in 5G Protocols: Evaluating Generative and Classification Models for Relation Extraction

To ensure the security and reliability of 5G wireless communication protocols, formal verification is employed to guarantee protocol correctness. Given the complexity and scale of 3GPP protocols, automating the formal modeling process is essential, as it can help security experts extract formal properties and dependencies and subsequently build the formal code. This paper introduces a novel Cross-Attention Large Language Model (CAL), a unique classification model specifically designed for this purpose. Additionally, we compare CAL to our augmented generative model based on the state-of-the-art Relation Extraction by End-to-End Language Generation (REBEL) framework. Both CAL and REBEL are evaluated on their ability to extract formal relationships from protocol documents, significantly reducing manual modeling efforts by over 95% on datasets such as DocRED and annotated 3GPP 5G protocols, including sessions of RRC connection establishment, initial AS security activation and et al. The study highlights the strengths, weaknesses, and optimal application scenarios for each model. The results demonstrate the feasibility of automating formal verification for complex communication protocols, ensuring their trustworthiness. This research marks a significant step towards the automation of formal verification, enhancing the robustness and reliability of 5G protocol design.