IP Library › Granted Patent US 12,621,337
Granted Patent B2
US 12,621,337 · App. 18/628,625 · Granted May 5, 2026

Amplification of formal method and fuzz testing to enable scalable assurance for communication system

Inventors: Ying Wang (West New York, NJ); Jingda Yang (Jersey City, NJ)
Assignee: The Trustees of the Stevens Institute of Technology
H04L63/1433G06F21/577G06F40/20G06N5/048G06F2221/033
View Patent ↗
Loading inventors, assignments & file history…
Monitor This Case
Get email alerts when status or documents change.
Order Certified Copies
Most orders are placed with the USPTO same day — all within 24 business hours.
Order via The Patent Place →
Pre-filled with this patent's details
Quick Facts
Patent No.
US 12,621,337
App. No.
18/628,625
Granted
May 5, 2026
Kind
B2
Abstract

Methods for more secure mobile network communications are disclosed. Specifically, details involving natural language processing (NLP) based auto formal modeling of protocols and specifications with large language models (NLP) are provided. Methods for formal and fuzzing amplification for fuzz testing to detect vulnerabilities are also disclosed. Furthermore, solutions are provided to identified vulnerabilities in existing 5G infrastructures. Also disclosed is a digital twin fuzzing framework.

Claims (51)

1 . A method for validating communication systems, comprising steps of:

obtaining input data comprising protocol descriptions;

transforming said protocol descriptions into dependency graphs and formal models using a large language model, said large language model being integrated with a transformer model;

resolving ambiguities in said input data;

determining design intent in said input data;

obtaining iterative feedback from a HyFuzz platform, said HyFuzz platform being adapted to refine capture of intentions and resolve ambiguities in said input data by providing said input data to said HyFuzz platform, wherein said HyFuzz platform is configured to supply said design intent to said large language model; and

producing output.

2 . The method of claim 1 , further comprising a step of establishing dependency relationships through cross-attention mechanisms and/or self-attention mechanisms.

3 . The method of claim 1 , further comprising a step of quantifying dependency relationships.

4 . The method of claim 3 , wherein said dependency relationships are quantified without human involvement.

5 . The method of claim 1 , further comprising a step of creating a list of exploits from said input data.

6 . The method of claim 5 , further comprising a step of conducting fuzz testing on said list of exploits.

7 . The method of claim 1 , wherein said large language model is Cross Attention Learning.

8 . The method of claim 1 , wherein said large language model performs concurrent processing of said protocol descriptions.

9 . The method of claim 1 , wherein said dependency graphs are scalable cross-session dependency graphs, supporting hierarchy of formal analysis, thereby facilitating revelation of in-depth relationships embedded within said protocol descriptions.

10 . The method of claim 1 , wherein said HyFuzz platform is trained on labeled identifiers and formal properties.

11 . The method of claim 1 , wherein said output bypasses token count barriers.

12 . A method for validating communication systems, comprising steps of:

obtaining input data comprising protocol descriptions;

transforming said protocol descriptions into dependency graphs and formal models using a large language model, said large language model being integrated with a transformer model:

resolving ambiguities in said input data;

determining design intent in said input data;

obtaining iterative feedback from an experimental platform by providing said input data to said experimental platform, wherein said experimental platform is configured to supply said design intent to said large language model; and

producing output, wherein said output bypasses token count barriers.

13 . The method of claim 12 , further comprising a step of establishing dependency relationships through cross-attention mechanisms and/or self-attention mechanisms.

14 . The method of claim 13 , further comprising a step of quantifying said dependency relationships.

15 . The method of claim 14 , wherein said dependency relationships are quantified without human involvement.

16 . The method of claim 12 , further comprising a step of creating a list of exploits from said input data.

17 . The method of claim 16 , further comprising a step of conducting fuzz testing on said list of exploits.

18 . The method of claim 12 , wherein said large language model performs concurrent processing of said protocol descriptions.

19 . The method of claim 12 , wherein said dependency graphs are scalable cross-session dependency graphs, supporting hierarchy of formal analysis, thereby facilitating revelation of in-depth relationships embedded within said protocol descriptions.

20 . The method of claim 12 , wherein the experimental platform is trained on labeled identifiers and formal properties.

21 . The method of claim 12 , wherein said large language model is Cross Attention Learning.

22 . A method for validating communication systems, comprising steps of:

obtaining input data comprising protocol descriptions;

transforming said protocol descriptions into dependency graphs and formal models using a large language model, said large language model being integrated with a transformer model;

resolving ambiguities in said input data;

determining design intent in said input data;

obtaining iterative feedback from an experimental platform by providing said input data to said experimental platform, wherein said experimental platform is configured to supply said design intent to said large language model;

producing output; and

determining if identifiers from said protocol descriptions inherit formal properties from previous identifiers of said protocol descriptions, thereby identifying direct and indirect dependency relationships.

23 . The method of claim 22 , wherein said direct and indirect dependency relationships are established through cross-attention mechanisms and/or self-attention mechanisms.

24 . The method of claim 22 , further comprising a step of quantifying said direct and indirect dependency relationships.

25 . The method of claim 24 , wherein said direct and indirect dependency relationships are quantified without human involvement.

26 . The method of claim 22 , further comprising a step of creating a list of exploits from said input data.

27 . The method of claim 26 , further comprising a step of conducting fuzz testing on said list of exploits.

28 . The method of claim 22 , wherein said large language model performs concurrent processing of said protocol descriptions.

29 . The method of claim 22 , wherein said output bypasses token count barriers.

30 . The method of claim 22 , wherein said dependency graphs are scalable cross-session dependency graphs, supporting hierarchy of formal analysis, thereby facilitating revelation of in-depth relationships embedded within said protocol descriptions.

31 . The method of claim 22 , wherein the experimental platform is trained on labeled identifiers and formal properties.

32 . The method of claim 22 , wherein said large language model is Cross Attention Learning.

Continuity (2)
Provisional Application 63457557 · Apr 6, 2023
Related Publication 20240340302A1 · Oct 10, 2024
References Cited (48)
US 11238542B1 · Wixted · 2022 [cited by examiner]
US 11593648B2 · Lee · 2023 [cited by examiner]
US 12434725B1 · Casterton · 2025 [cited by examiner]
US 20060274070A1 · Herman · 2006 [cited by examiner]
US 20210058970A1 · Kwak · 2021 [cited by examiner]
US 20210117617A1 · Blaya · 2021 [cited by examiner]
US 20220284235A1 · Jones · 2022 [cited by examiner]
US 20220329608A1 · Liu · 2022 [cited by examiner]
US 20220335135A1 · McGraw et al. · 2022 [cited by applicant]
US 20230094656A1 · Mukherjee · 2023 [cited by applicant]
US 20230123322A1 · Cella · 2023 [cited by examiner]
US 20230127651A1 · Cella · 2023 [cited by examiner]
US 20230196179A1 · Abraham · 2023 [cited by examiner]
US 20230222393A1 · Zahm · 2023 [cited by examiner]
US 20230298325A1 · Malur Srinivasan · 2023 [cited by examiner]
US 20230319086A1 · Beauchesne · 2023 [cited by applicant]
US 20240187176A1 · Wang · 2024 [cited by examiner]
US 20240242428A1 · Ackerman · 2024 [cited by examiner]
US 20240249158A1 · Narayanan · 2024 [cited by examiner]
US 20240256948A1 · Betthauser · 2024 [cited by examiner]
US 20240330655A1 · Hearty · 2024 [cited by examiner]
US 20240333765A1 · McGrew · 2024 [cited by examiner]
US 20240338458A1 · Wang et al. · 2024 [cited by applicant]
US 20240340302A1 · Wang · 2024 [cited by examiner]
US 20240388540A1 · Bush · 2024 [cited by examiner]
US 20240403428A1 · Lal · 2024 [cited by examiner]
US 20240414211A1 · Boyer · 2024 [cited by examiner]
US 20250007926A1 · Southgate · 2025 [cited by examiner]
US 20250111150A1 · Garapati · 2025 [cited by examiner]
US 20250227119A1 · Abbaszadeh · 2025 [cited by examiner]
US 20250231973A1 · Kelsey · 2025 [cited by examiner]
CN 116150684B · 2024 [cited by examiner]
Abdo et al., “Ensured Confidentiality Authentication and Key Agreement Protocol for Eps,” in 2012 Symposium on Broadband etworks and Fast Internet, RELABIRA, May 28-29, 2012. [cited by applicant]
Clarke et al., “Counterexample-guided Abstraction Refinement,” CAV 2000, LNCS 1855, Springer-Verlag Berlin Heidelberg, 2000,154-169. [cited by applicant]
Cremers et al., “Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion,” Network and Distributed System Security Symposium, Jan. 2019. [cited by applicant]
Hadj-Kacem et al., “A Formal Model of a Multi-step Coordination Protocol for Self-adaptive Software Using Coloured Petri Nets,” International Journal of Computing and Information Sciences (IJCIS), http://www.ijcis.info/… [cited by applicant]
Khan et al., “Defeating the Downgrade Attack on Identity Privacy in 5g,” in International Conference on Research in Security Standardisation, Springer, 2018. [cited by applicant]
Universal Mobile Telecommunications System (UMTS); LTE; Mobility Management Entity (MME)—Visitor Location Register (VLR), SGs Interface Specification, 3rd Generation Partnership Project (3GPP), Apr. 9, 2018, 79 pages. [cited by applicant]
Vaswani et al., “Attention is all you need,” 31st Conference on Neural Information Processing Systems (NIPS 2017), 2017, 11 pages. [cited by applicant]
Yang, “Vulnerability and Unintended Emergent Behavior Detection for 5G RRC Protocols and Stack Journal Version,” IEEE Journal on Selected Areas in Communications, Feb. 9, 2023. [cited by applicant]
Yang et al., “Dependency-Graph enabled Formal Analysis for 5G AKA Protocols: Assumption Propagation and Verification,” Accepted at 2024 IEEE International Conference on Communications (ICC), Jan. 2024, 7 pages plus cove… [cited by applicant]
Yang et al., “Systematic Meets Unintended: Prior Knowledge Adaptive 5G Vulnerability Detection via Multi-Fuzzing,” Journal of Latex Class Files, IEEE, 2021, 1-15. [cited by applicant]
Yang et al., “Toward Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal Cross-and-Self-Attention Large Language Model Approach,” IEEE Access, vol. 12, Feb. 26, 2024, 12 pages. [cited by applicant]
Yang et al., “Systematic and Scalable Vulnerability Detection for 5G Specifications and Implementations,” IEEE Journal on Selected Areas in Communications, 2023, 1-11. [cited by applicant]
Abdo et al., “Ensured Confidentiality Authentication and Key Agreement Protocol for EPS,” 2012 Symposium on Broadband Networks and Fast Internet (RELABIRA), IEEE, 2012, 5 pages. [cited by applicant]
Cremers et al., “Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion,” Network and Distributed System Security (NDSS) Symposium 2019, Feb. 24-27, 2019, San Diego, USA, 15 pages. [cited by applicant]
Khan et al., “Defeating the Downgrade Attack on Identity Privacy in 5G,” Springer Nature Switzerland AG 2018, 95-119. [cited by applicant]
Office Action issued for U.S. Appl. No. 18/628,619 entitled “Amplification of Formal Method and Fuzz Testing to Enable Scalable Assurance for Communication System,” dated Sep. 4, 2025, 30 pages. [cited by applicant]