CN-122027223-A - Knowledge injection-based security protocol modeling method and related device

CN122027223ACN 122027223 ACN122027223 ACN 122027223ACN-122027223-A

Abstract

The application provides a knowledge injection-based safety protocol modeling method and a related device, which are characterized in that a semantic analysis is carried out on a natural language protocol description to extract key elements in a protocol structure, an intermediate representation is constructed, a candidate model is selected and obtained based on similarity between the intermediate representation and a knowledge graph of a safety protocol, a modeling prompt template is obtained by fusing a protocol skeleton, a knowledge example and formal grammar constraint, an initial formal model is generated according to the modeling prompt template, grammar verification and formal verification are carried out on the initial formal model, the initial formal model is revised to obtain a target model, and automatic construction and optimization from unstructured protocol specification to verifiable model are realized by introducing a domain knowledge graph, structuring the intermediate representation and a feedback mechanism based on a verifier, so that the automatic generation, verification and optimization of the protocol model are realized, and modeling quality and engineering practicability are improved.

Inventors

Lin Yajia
SU JIE
TIAN CONG
DUAN ZHENHUA

Assignees

西安电子科技大学广州研究院
西安电子科技大学

Dates

Publication Date: 20260512
Application Date: 20260113

Claims (10)

1. A knowledge injection-based security protocol modeling method, comprising: Acquiring a natural language protocol description; carrying out semantic analysis on the natural language protocol description, extracting key elements in protocol participants, initial knowledge, message interaction flow and security attribute description information, and constructing to obtain intermediate representation; Based on the semantic similarity and the structural similarity between the intermediate representation and the knowledge graph of the security protocol, matching the protocol model in the knowledge graph, and selecting to obtain a candidate model; obtaining a protocol skeleton according to the intermediate representation, obtaining a knowledge example according to the candidate model, fusing the protocol skeleton, the knowledge example and formal grammar constraint to obtain a modeling prompt template, and generating an initial formal model according to the modeling prompt template; and carrying out grammar verification and formal verification on the initial formal model by using a calling tool, inputting a verification result as structural feedback information into a large language model for generating the initial formal model, and correcting the initial formal model by using a driver until a target model passing verification is obtained.
2. The knowledge injection based security protocol modeling method of claim 1, wherein the intermediate representation is a structured data representation.
3. The knowledge injection-based security protocol modeling method according to claim 1, wherein the knowledge graph of the security protocol stores validated protocol models, and associates semantic enhanced semantic annotation information for each protocol model for characterizing rule semantics, variable dependency relationships, and security attributes.
4. The knowledge injection-based security protocol modeling method according to claim 1, wherein the matching the protocol model in the knowledge graph based on the semantic similarity and the structural similarity between the intermediate representation and the knowledge graph of the security protocol, and selecting to obtain the candidate model comprises: the semantic similarity and the structural similarity between the intermediate representation and the knowledge graph of the security protocol obtain a total similarity score; matching the protocol models in the knowledge graph based on the total similarity score, and selecting to obtain candidate models; the overall similarity score is expressed as: In the formula (I), in the formula (II), Score for total similarity; For the purpose of semantic similarity, In order for the structural similarity to be of a similar nature, Is a weight coefficient of the semantic similarity, Is a weight coefficient of the structural similarity.
5. The knowledge injection based security protocol modeling method of claim 1, wherein deriving knowledge instances from the candidate models comprises: Carrying out semantic enhancement processing on the candidate model to obtain first semantic enhancement information for transfer learning; Carrying out abstract coding processing on the first semantic enhancement information to generate second semantic enhancement information for guiding protocol modeling; And combining the first semantic enhancement information, the second semantic enhancement information and the candidate model to form a knowledge example for modeling the large language model.
6. The method of claim 1, wherein the initial formal model includes at least message interaction rules for describing protocol execution, equation or function definitions for constraining protocol behavior, and security quotation description information for expressing protocol security objectives.
7. The knowledge injection based security protocol modeling method of claim 1, wherein the performing a grammar check on the initial formal model comprises: and calling a formal verification tool to perform static grammar checking on the initial formal model, and when grammar errors exist in the initial formal model, feeding back an error report to a large language model for generating the initial formal model, so that the large language model corrects the initial formal model according to the error report.
8. The knowledge injection based security protocol modeling method of claim 1, wherein formalizing validating the initial formalized model comprises: Performing formal verification on the safety quotation in the initial formal model based on a formal tool, and evaluating the passing rate and the structural correctness of the quotation; When any security primer fails to pass the verification, the corresponding verification failure log is used as structured feedback information to be input into a large language model for generating an initial formal model, so that the large language model is driven to carry out logic correction processing on the protocol rule, the variable dependence relation or the security primer of the initial formal model according to the verification failure log.
9. An electronic device comprising a memory, a processor and a computer program stored on the memory and executable on the processor, the processor implementing the knowledge injection based security protocol modeling method of any of claims 1 to 8 when the computer program is executed.
10. A computer storage medium having stored thereon computer executable instructions for performing the knowledge injection based security protocol modeling method of any of claims 1 to 8.

Description

Knowledge injection-based security protocol modeling method and related device Technical Field The embodiment of the application relates to the field of modeling, in particular to a security protocol modeling method based on knowledge injection and a related device. Background The security protocol is a key technology for guaranteeing confidentiality, integrity and authenticability in the network communication process, and the correctness of the security protocol is directly related to the overall security level of the information system. However, in the actual design and implementation process, the security protocol attempts to implicate complex security assumptions, state dependencies, and attacker model constraints, so that it is difficult for protocol designers to comprehensively discover potential logic defects and potential safety hazards through conventional test means. Thus, formal verification techniques are widely used for systematically verifying security properties and anti-attack capabilities of security protocols. Tamarin Prover is one of the currently mainstream security protocol-form validation tools that is capable of automated reasoning and validation of security attributes in a protocol based on a multiset rewrite rule and constraint solving mechanism. However, the Tamarin modeling process has very strict requirements on rule structures, grammar formats and semantic constraints, the model writing needs to have stronger formalized modeling capability and protocol analysis experience, the manual modeling process has huge workload, verification failure is extremely easy to be caused by rule omission, semantic misunderstanding or grammar errors, and the application of security protocol formalized verification in actual engineering is severely restricted. However, the formal model for assisting in generating the security protocol by using the large language model still has the following problems that the support of field security knowledge is lacking, the implicit security semantics and the dependency relationship in the protocol are difficult to identify, the complete structural modeling elements cannot be automatically constructed from the natural language description, the generated Tamrin model has high grammar error rate and insufficient structure normalization, and the automatic conversion from the natural language security protocol specification to the verifiable Tamarin model is realized on the premise that the grammar correctness, the semantic consistency and the structure integrity cannot be ensured, the modeling efficiency is low and the stability is poor due to the serious dependence on manual participation and field experience. Disclosure of Invention The following is a summary of the subject matter described in detail herein. The application aims to solve one of the technical problems existing in the related art to at least a certain extent, and the embodiment of the application provides a security protocol modeling method and a related device based on knowledge injection, which can improve the accuracy, the integrity and the efficiency of security protocol modeling. An embodiment of the first aspect of the present application is a security protocol modeling method based on knowledge injection, including: Acquiring a natural language protocol description; carrying out semantic analysis on the natural language protocol description, extracting key elements in protocol participants, initial knowledge, message interaction flow and security attribute description information, and constructing to obtain intermediate representation; Based on the semantic similarity and the structural similarity between the intermediate representation and the knowledge graph of the security protocol, matching the protocol model in the knowledge graph, and selecting to obtain a candidate model; obtaining a protocol skeleton according to the intermediate representation, obtaining a knowledge example according to the candidate model, fusing the protocol skeleton, the knowledge example and formal grammar constraint to obtain a modeling prompt template, and generating an initial formal model according to the modeling prompt template; and carrying out grammar verification and formal verification on the initial formal model by using a calling tool, inputting a verification result as structural feedback information into a large language model for generating the initial formal model, and correcting the initial formal model by using a driver until a target model passing verification is obtained. According to certain embodiments of the first aspect of the present application, the intermediate representation is a structured data representation. According to certain embodiments of the first aspect of the present application, the knowledge graph of the security protocol stores validated protocol models, and for each protocol model, semantic enhanced semantic annotation information for characterizing rule semantics, vari