CN114500347B - Method and system for formalized verification of security interconnection protocol - Google Patents
Method and system for formalized verification of security interconnection protocol Download PDFInfo
- Publication number
- CN114500347B CN114500347B CN202210402333.1A CN202210402333A CN114500347B CN 114500347 B CN114500347 B CN 114500347B CN 202210402333 A CN202210402333 A CN 202210402333A CN 114500347 B CN114500347 B CN 114500347B
- Authority
- CN
- China
- Prior art keywords
- protocol
- security
- modeling
- rule
- message
- Prior art date
- Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
- Active
Links
- 238000000034 method Methods 0.000 title claims abstract description 102
- 238000012795 verification Methods 0.000 title claims abstract description 96
- 230000007704 transition Effects 0.000 claims description 40
- 230000008569 process Effects 0.000 claims description 35
- 238000012545 processing Methods 0.000 claims description 18
- 238000004422 calculation algorithm Methods 0.000 claims description 14
- 238000012163 sequencing technique Methods 0.000 claims description 14
- 238000004590 computer program Methods 0.000 claims description 11
- 230000007547 defect Effects 0.000 claims description 9
- 238000013461 design Methods 0.000 claims description 9
- 238000012546 transfer Methods 0.000 claims description 9
- 230000009471 action Effects 0.000 claims description 8
- 238000005094 computer simulation Methods 0.000 claims description 7
- 238000013508 migration Methods 0.000 claims description 4
- 230000005012 migration Effects 0.000 claims description 4
- 238000004880 explosion Methods 0.000 abstract description 8
- 238000010586 diagram Methods 0.000 description 15
- 238000001514 detection method Methods 0.000 description 13
- 238000004891 communication Methods 0.000 description 10
- 238000010200 validation analysis Methods 0.000 description 7
- 238000013475 authorization Methods 0.000 description 6
- 230000006399 behavior Effects 0.000 description 5
- 238000004458 analytical method Methods 0.000 description 4
- 238000005516 engineering process Methods 0.000 description 4
- 230000006870 function Effects 0.000 description 4
- 230000003993 interaction Effects 0.000 description 4
- 230000004044 response Effects 0.000 description 4
- 241000288961 Saguinus imperator Species 0.000 description 3
- 230000008901 benefit Effects 0.000 description 3
- 238000004364 calculation method Methods 0.000 description 3
- RCRODHONKLSMIF-UHFFFAOYSA-N isosuberenol Natural products O1C(=O)C=CC2=C1C=C(OC)C(CC(O)C(C)=C)=C2 RCRODHONKLSMIF-UHFFFAOYSA-N 0.000 description 3
- 230000005540 biological transmission Effects 0.000 description 2
- 230000001364 causal effect Effects 0.000 description 2
- 238000010998 test method Methods 0.000 description 2
- 238000012360 testing method Methods 0.000 description 2
- 230000006978 adaptation Effects 0.000 description 1
- 230000003542 behavioural effect Effects 0.000 description 1
- 230000008859 change Effects 0.000 description 1
- 230000001276 controlling effect Effects 0.000 description 1
- 238000012937 correction Methods 0.000 description 1
- 230000000875 corresponding effect Effects 0.000 description 1
- 238000009795 derivation Methods 0.000 description 1
- 238000011161 development Methods 0.000 description 1
- 238000005538 encapsulation Methods 0.000 description 1
- 239000004973 liquid crystal related substance Substances 0.000 description 1
- 238000012423 maintenance Methods 0.000 description 1
- 238000012986 modification Methods 0.000 description 1
- 230000004048 modification Effects 0.000 description 1
- 238000012544 monitoring process Methods 0.000 description 1
- 238000005457 optimization Methods 0.000 description 1
- HRULVFRXEOZUMJ-UHFFFAOYSA-K potassium;disodium;2-(4-chloro-2-methylphenoxy)propanoate;methyl-dioxido-oxo-$l^{5}-arsane Chemical compound [Na+].[Na+].[K+].C[As]([O-])([O-])=O.[O-]C(=O)C(C)OC1=CC=C(Cl)C=C1C HRULVFRXEOZUMJ-UHFFFAOYSA-K 0.000 description 1
Images
Classifications
-
- H—ELECTRICITY
- H04—ELECTRIC COMMUNICATION TECHNIQUE
- H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
- H04L43/00—Arrangements for monitoring or testing data switching networks
- H04L43/18—Protocol analysers
-
- H—ELECTRICITY
- H04—ELECTRIC COMMUNICATION TECHNIQUE
- H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
- H04L41/00—Arrangements for maintenance, administration or management of data switching networks, e.g. of packet switching networks
- H04L41/14—Network analysis or design
- H04L41/145—Network analysis or design involving simulating, designing, planning or modelling of a network
-
- H—ELECTRICITY
- H04—ELECTRIC COMMUNICATION TECHNIQUE
- H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
- H04L63/00—Network architectures or network communication protocols for network security
- H04L63/04—Network architectures or network communication protocols for network security for providing a confidential data exchange among entities communicating through data packet networks
- H04L63/0428—Network architectures or network communication protocols for network security for providing a confidential data exchange among entities communicating through data packet networks wherein the data content is protected, e.g. by encrypting or encapsulating the payload
-
- H—ELECTRICITY
- H04—ELECTRIC COMMUNICATION TECHNIQUE
- H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
- H04L63/00—Network architectures or network communication protocols for network security
- H04L63/14—Network architectures or network communication protocols for network security for detecting or protecting against malicious traffic
- H04L63/1408—Network architectures or network communication protocols for network security for detecting or protecting against malicious traffic by monitoring network traffic
- H04L63/1416—Event detection, e.g. attack signature detection
Landscapes
- Engineering & Computer Science (AREA)
- Computer Security & Cryptography (AREA)
- Computer Networks & Wireless Communication (AREA)
- Signal Processing (AREA)
- Computer Hardware Design (AREA)
- Computing Systems (AREA)
- General Engineering & Computer Science (AREA)
- Computer And Data Communications (AREA)
- Data Exchanges In Wide-Area Networks (AREA)
Abstract
The invention provides a method and a system for formalized verification of a security interconnection protocol, belongs to the field of protocol verification, and aims to solve the problems of state space explosion, low automation degree of protocol verification and incapability of acquiring protocol attack conditions in formal verification of a network security protocol. The method comprises the following steps: step S1, obtaining a security interconnection protocol to be verified, and modeling the security interconnection protocol to be verified to obtain a security interconnection protocol model, where the modeling includes: modeling encrypted messages, modeling a concurrent system, modeling protocol deduction rules and describing protocol tracking; step S2, based on the security interconnection protocol model and the security attribute of the preset security interconnection protocol, executing formal verification on the security interconnection protocol to be verified, and obtaining a verification result.
Description
Technical Field
The invention belongs to the field of protocol verification, and particularly relates to a method and a system for performing formal verification on a secure interconnection protocol.
Background
At present, with the development of the internet, network security becomes a topic of concern more and more. An attacker in the network can influence the communication content in a reading, tampering, deleting, monitoring and other modes, and even can attack and control a plurality of network entities simultaneously. The network security protocol is a protocol for ensuring security of data communication between terminals by performing key distribution, identity authentication, and the like on a network through related technologies of cryptography. The network security protocol can defend most attacks, but when the protocol faces complicated and changeable network conditions and the assumed network operation condition is changed during the original protocol design, the security of the network security protocol cannot be guaranteed. Therefore, the network security protocol as a system standard of the information exchange rule between the protocol using the subjects needs not only reasonable design but also some way to analyze and verify the security.
The secure interconnection Protocol (DSCP) is a network Protocol for realizing the functions of automatic discovery of a Protocol using main body, secure Access authentication, virtual channel establishment and flow control, data adaptation encapsulation, anti-replay, ciphertext transmission, link maintenance and detection, transmission error correction control, anti-replay and the like, and can be matched with an upper layer control Protocol to effectively prevent illegal Protocol from using main body Access, avoid the Protocol using main body from receiving multi-layer attacks from Access control to message forwarding, provide identity Security identification for the upper layer network Protocol, and provide a secure interaction means for controlling, managing and service messages between the main bodies used by a private network Protocol.
The formalization method is a method for verifying the security of a target system through defined stipulations and proofs. It is based on a formalized mathematical system and uses symbolic definitions and models to build a constructed symbolic model. The formalization method can be applied to analyzing the security of the network security protocol, and analyzes and verifies the security of the network security protocol by simulating various conditions of network operation through detailed analysis of various attack paths of attackers. The formalization method has the advantages of being capable of modeling the network environment more efficiently and finding out the safety problems which can occur when the safety protocol is applied.
At present, formal verification methods for network security protocols are mainly divided into three types, namely modal logic, model detection and theorem proving.
(1) The modal logic mainly comprises propositions and reasoning, initial propositions believed by each subject are described by establishing a protocol model description through protocol idealization, giving initial assumptions, establishing message assertion rules and the like, final propositions are obtained from the respective initial propositions through a logic reasoning method such as BAN logic through a logic derivation process, and vulnerabilities existing in the network security protocol are discovered through analyzing the final propositions.
(2) Theorem proving mainly comprises two steps of stipulation and proving. Firstly, formalizing and stipulating a network security protocol rule, firstly describing a protocol participant type, a protocol communication message type and a protocol behavior type, and then analyzing and describing a protocol target security attribute to obtain a security attribute stipulation required to be met by a protocol. Finally, the system is proved to meet the target property, so that the verified network security protocol is obtained.
(3) The model detection is a method for carrying out automatic certification through a finite state concurrent system, and formalized verification work is completed through a protocol analysis tool. Firstly, describing a state space of a network security protocol by using a state machine model, and then determining whether a potential attacker reachable path exists by using an automatic state space searching method.
The model detection has the characteristics of high automation degree, and counter examples can be conveniently obtained in the verification process. The main drawback of the model detection technique is the presence of the state space explosion problem. FIG. 1 is a diagram illustrating a prior art network security protocol authentication scheme; as shown in fig. 1, model detection formalizes a protocol as a finite state concurrent system, describes the protocol rules, system properties, and behavioral descriptions of protocol attackers through the description of the protocol rules and instantiating protocol participants. During verification, a specific model detection tool is used for searching the state space of the model, whether an example violating the inverse model convention and the system property exists in the state space is verified, and if the detection tool gives a counter example, the explanation convention is not true. The existing network security protocol verification based on the model detection technology mainly has the following problems: 1. when the number of protocol participants is too large, the protocol concurrency causes the explosion problem of the model state space, and the problem that the attribute cannot be verified exists. 2. The verification degree is low, and a large amount of false counter-example false alarms exist. 3. No formal model of the attacker is built.
Disclosure of Invention
The invention provides a scheme for carrying out formal verification on a safety interconnection protocol, which is based on actual requirements, aims at solving the problems of the prior network safety protocol formal verification technology, such as state space explosion, low automation degree of protocol verification, incapability of acquiring protocol attack conditions and the like, and analyzes and verifies the safety of the safety interconnection protocol.
The invention discloses a method for formally verifying a secure interconnection protocol in a first aspect. The security interconnection protocol is a network security protocol working on a link layer and is used for cooperating with an upper control protocol to resist the attack introduced by an illegal protocol through the access of a main body; the method comprises the following steps:
step S1, obtaining a security interconnection protocol to be verified, and modeling the security interconnection protocol to be verified to obtain a security interconnection protocol model, where the modeling includes: modeling encrypted messages, modeling a concurrent system, modeling protocol deduction rules and describing protocol tracking;
step S2, based on the security interconnection protocol model and the security attribute of the preset security interconnection protocol, executing formal verification of the security interconnection protocol to be verified, and acquiring a verification result;
wherein, in the step S1:
the encrypted message is modeled as: modeling an encrypted message used in the security interconnection protocol to be verified to acquire an encryption rule, an attribute description and a message value of the encrypted message;
the concurrent system is modeled as: modeling a system state set, a system state transition rule and a system state operation semantic of the to-be-verified security interconnection protocol during concurrence execution so as to simulate concurrence states of a user and an attacker during concurrence execution;
the protocol deduction rule is modeled as follows: describing a message deduction rule of the to-be-verified secure interconnection protocol, wherein the message deduction rule comprises a protocol rule description commonly owned by a protocol participant and the attacker, and a protocol message deduction rule description owned by the attacker but not owned by the protocol participant;
the protocol trace is described as: and sequencing system actions according to time points to obtain a tracking track, thereby completing protocol tracking description of the to-be-verified security interconnection protocol.
According to the method of the first aspect of the invention, in the process of modeling the encrypted message: the encryption rules comprise one or more of encryption algorithm, decryption algorithm, key design rule and random number rule; the attribute description includes: whether information is leaked to an unauthorized entity, whether the information is modified by the unauthorized entity, whether a message sender is an original sender, and whether the sent message is modified; the message values include: public key, private key, encrypted message.
According to the method of the first aspect of the present invention, in the process of modeling the concurrent system, the modeling of the concurrent system is completed by symbolically describing a system state transition rule in a multi-set rewrite manner, which specifically includes:
modeling a to-be-generated transfer state of the system according to the actual running condition of the system so as to obtain the system state set when the concurrency is executed;
describing the system state transition rules by using an inference rule representation method in a multi-set rewriting mode, wherein the inference rule representation method comprises a current state, a transition condition and a next state;
and describing the operation semantics of the system state transition rule as the system state operation semantics.
According to the method of the first aspect of the present invention, in the protocol deduction rule modeling process:
the protocol rule description commonly owned by the protocol participant and the attacker comprises: symbol description of specific facts in the security interconnection protocol to be verified and a key rule messaging rule;
the protocol message deduction rule description possessed by the attacker but not possessed by the protocol participant comprises the following steps: the system comprises a protocol deduction capability of an attacker, a protocol deduction capability of the attacker, wherein the attacker receives a message from a protocol sending party and sends the received message to a protocol receiving party, the protocol deduction capability of the attacker, wherein the message sending operation of the attacker can be tracked, the attacker is allowed to acquire the protocol deduction capability of the latest system state at any time, the attacker is allowed to influence the protocol deduction capability of the system state by tampering the message, and the attacker can carry out special processing and deduction the protocol deduction capability of the message.
According to the method of the first aspect of the invention, during the protocol trace description: and introducing the time point as a protocol tracking attribute to describe a tracking formula, and sequencing each operation completed in the state space search through the time point to describe a semantic process of the tracking formula so as to obtain the tracking track.
According to the method of the first aspect of the present invention, the security attribute of the preset security interconnection protocol is the security attribute of the security interconnection protocol to be verified, formal verification is performed on the security interconnection protocol to be verified by using a protocol verification tool, when the security interconnection protocol to be verified satisfies the security attribute of the preset security interconnection protocol, it is determined that no security defect exists, otherwise, attack is positioned according to a counter-example.
The invention discloses a system for formally verifying a secure interconnection protocol in a second aspect. The safety interconnection protocol is a network safety protocol working on a link layer and is used for cooperating with an upper control protocol to resist the attack introduced by an illegal protocol through the access of a main body; the system comprises:
a first processing unit configured to: the method comprises the steps of obtaining a to-be-verified security interconnection protocol, and modeling the to-be-verified security interconnection protocol to obtain a security interconnection protocol model, wherein the modeling comprises the following steps: modeling encrypted messages, modeling a concurrent system, modeling protocol deduction rules and describing protocol tracking;
a second processing unit configured to: based on the security interconnection protocol model and the security attributes of a preset security interconnection protocol, executing formal verification of the security interconnection protocol to be verified, and acquiring a verification result;
wherein the first processing unit is specifically configured to:
the encrypted message is modeled as: modeling an encrypted message used in the to-be-verified security interconnection protocol to acquire an encryption rule, an attribute description and a message value of the encrypted message;
the concurrent system is modeled as: modeling a system state set, a system state transition rule and a system state operation semantic of the to-be-verified security interconnection protocol during concurrence execution so as to simulate concurrence states of a user and an attacker during concurrence execution;
the protocol deduction rule is modeled as follows: describing a message deduction rule of the to-be-verified secure interconnection protocol, wherein the message deduction rule comprises a protocol rule description commonly owned by a protocol participant and the attacker, and a protocol message deduction rule description owned by the attacker but not owned by the protocol participant;
the protocol trace is described as: and sequencing system actions according to time points to obtain a tracking track, thereby completing protocol tracking description of the to-be-verified security interconnection protocol.
According to the system of the second aspect of the invention, in the process of modeling the encrypted message: the encryption rules comprise one or more of encryption algorithm, decryption algorithm, key design rule and random number rule; the attribute description includes: whether information is leaked to an unauthorized entity, whether the information is modified by the unauthorized entity, whether a message sender is an original sender, and whether the sent message is modified; the message values include: public key, private key, encrypted message.
According to the system of the second aspect of the present invention, in the process of modeling the concurrent system, the modeling of the concurrent system is completed by symbolically describing a system state transition rule in a multi-set rewrite manner, which specifically includes:
modeling a to-be-generated transfer state of the system according to the actual running condition of the system so as to obtain the system state set when the concurrency is executed;
describing the system state transition rule by using an inference rule representation method in a multi-set rewriting mode, wherein the system state transition rule comprises a current state, a transition condition and a next state;
and describing the operation semantics of the system state transition rule as the system state operation semantics.
According to the system of the second aspect of the present invention, in the protocol deduction rule modeling:
the protocol rule description commonly owned by the protocol participant and the attacker comprises: symbol description of specific facts in the security interconnection protocol to be verified and a key rule messaging rule;
the protocol message deduction rule description possessed by the attacker but not possessed by the protocol participant comprises: the system comprises a protocol deduction capability of an attacker, a protocol deduction capability of the attacker, wherein the attacker receives a message from a protocol sending party and sends the received message to a protocol receiving party, the protocol deduction capability of the attacker, wherein the message sending operation of the attacker can be tracked, the attacker is allowed to acquire the protocol deduction capability of the latest system state at any time, the attacker is allowed to influence the protocol deduction capability of the system state by tampering the message, and the attacker can carry out special processing and deduction the protocol deduction capability of the message.
According to the system of the second aspect of the present invention, in the process of the protocol trace description: and introducing the time point as a protocol tracking attribute to describe a tracking formula, and sequencing each operation completed in the state space search through the time point to describe a semantic process of the tracking formula so as to obtain the tracking track.
According to the system of the second aspect of the present invention, the security attribute of the preset secure interconnection protocol is the security attribute of the secure interconnection protocol to be verified, and the second processing unit is specifically configured to: and performing formal verification on the to-be-verified security interconnection protocol by using a protocol verification tool, judging that no security defect exists when the to-be-verified security interconnection protocol meets the security attribute of the preset security interconnection protocol, and otherwise, positioning the attack according to the counter example.
A third aspect of the invention discloses an electronic device. The electronic device comprises a memory and a processor, wherein the memory stores a computer program, and the processor implements the steps of the method for formally verifying the secure interconnection protocol according to any one of the first aspect of the disclosure when executing the computer program.
A fourth aspect of the invention discloses a computer-readable storage medium. The computer readable storage medium has stored thereon a computer program which, when executed by a processor, implements the steps of a method for formal verification of a secure interconnect protocol according to any of the first aspect of the present disclosure.
In conclusion, the technical scheme provided by the invention has high automation degree for verifying the safety interconnection protocol, the protocol parallel condition can be effectively proved, the labor cost is greatly reduced, the user can complete the verification work of the safety protocol without extremely high logical reasoning capability, and the use threshold of a formalized tool is reduced. The complexity of the state space is reduced by methods such as Applied Pi calculation and the like, the problem of explosion of the state space is avoided, and the verification speed is improved. Through modeling of the attacker deduction rule, the behavior formalization model of the attacker is described and verified, and the safety of the protocol can be analyzed more completely. The tracking formula is described by introducing the time points as the tracking attributes, so that the tracking track of the protocol can be obtained after the time points are sequenced, the false alarm rate of counter cases is reduced, and the verification efficiency is improved.
Drawings
In order to more clearly illustrate the embodiments or prior art solutions of the present invention, the drawings used in the embodiments or prior art descriptions will be briefly described below, it is obvious that the drawings in the following description are some embodiments of the present invention, and other drawings can be obtained by those skilled in the art without inventive efforts.
FIG. 1 is a diagram illustrating a prior art network security protocol authentication scheme;
FIG. 2 is a flow diagram of a method for formalized validation of a secure interconnect protocol in accordance with an embodiment of the present invention;
fig. 3 is a diagram illustrating an implementation of the TLS1.3 handshake protocol according to an embodiment of the present invention;
FIG. 4 is a dependency graph introduced at time of protocol validation according to an embodiment of the present invention;
FIG. 5 is a diagram illustrating formal verification of a secure interconnect protocol according to a first embodiment of the present invention;
fig. 6 is a schematic diagram of a tamarind-driver-based formal verification of a secure interconnect protocol according to a third embodiment of the present invention;
FIG. 7 is a block diagram of a method for formalized validation of a secure interconnect protocol in accordance with an embodiment of the present invention;
fig. 8 is a block diagram of an electronic device according to an embodiment of the present invention.
Detailed Description
In order to make the objects, technical solutions and advantages of the embodiments of the present invention clearer, the technical solutions in the embodiments of the present invention will be clearly and completely described below with reference to the drawings in the embodiments of the present invention. All other embodiments, which can be obtained by a person skilled in the art without making any creative effort based on the embodiments in the present invention, belong to the protection scope of the present invention.
The invention discloses a method for formalized verification of a secure interconnection protocol in a first aspect. The safety interconnection protocol is a network safety protocol working on a link layer and is used for cooperating with an upper control protocol to resist the attack introduced by an illegal protocol through the access of a main body; FIG. 2 is a flow diagram of a method for formalized validation of a secure interconnect protocol in accordance with an embodiment of the present invention; as shown in fig. 2, the method includes:
step S1, obtaining a security interconnection protocol to be verified, and modeling the security interconnection protocol to be verified to obtain a security interconnection protocol model, where the modeling includes: modeling encrypted messages, modeling a concurrent system, modeling protocol deduction rules and describing protocol tracking;
step S2, based on the security interconnection protocol model and the security attribute of the preset security interconnection protocol, executing formal verification on the security interconnection protocol to be verified, and obtaining a verification result.
In some embodiments, the encrypted message is modeled as: and modeling the encrypted message used in the to-be-verified security interconnection protocol to acquire an encryption rule, an attribute description and a message value of the encrypted message.
Specifically, in the process of modeling the encrypted message: the encryption rules comprise one or more of encryption algorithm, decryption algorithm, key design rule and random number rule; the attribute description includes: whether information is leaked to an unauthorized entity, whether the information is modified by the unauthorized entity, whether a message sender is an original sender, and whether the sent message is modified; the message values include: public key, private key, encrypted message.
In particular, in the attribute description, descriptions of Confidentiality, Integrity, and Authentication are referred to. Wherein Confidentiality indicates that if the information content is not revealed to an unauthorized entity, it is confidential; integrity indicates that the information is complete if it has not been modified by any unauthorized entity; authentication indicates that authorization is granted if the sender of the message is indeed the original sender and the message is unchanged.
Specifically, the encrypted messages are modeled for the secure interconnection protocol, and the encrypted messages involved in the use process of the secure interconnection protocol are modeled. The method comprises the steps of taking rules related to protocol messages, such as rules of encryption and decryption algorithm, message key design, random numbers and the like as input, modeling the encrypted messages by using an ordered algebra and equation correlation theory method, obtaining attribute description of an encrypted message model, and obtaining the encrypted message model. Such as unencrypted text, the participant can obtain public and private keys, and encrypted messages, etc. after entering the model.
In some embodiments, the concurrent system is modeled as: modeling a system state set, a system state transition rule and a system state operation semantic of the to-be-verified security interconnection protocol during concurrent execution so as to simulate concurrent states of a user and an attacker during concurrent execution.
Specifically, in the process of modeling the concurrent system, the concurrent system modeling is completed by symbolically describing a system state transition rule in a multi-set rewriting manner, and specifically includes: modeling a to-be-generated transfer state of the system according to the actual running condition of the system so as to obtain the system state set when the concurrency is executed; describing the system state transition rules by using an inference rule representation method in a multi-set rewriting mode, wherein the inference rule representation method comprises a current state, a transition condition and a next state; and describing the operation semantics of the system state transition rule as the system state operation semantics.
Specifically, a secure interconnect protocol is concurrently system modeled. In order to support the situation that a protocol authorization participant and a multi-party user such as a protocol attacker and the like are concurrent in the protocol running process, a concurrent system of the protocol needs to be modeled, the concurrent execution of the protocol authorization user and an opponent attacker is described by using a multi-set rewriting method, and when the concurrent execution of the protocol occurs, the state of the system needs to be subjected to concurrent multi-set rewriting change, and a new system state is created. In order to establish a concurrent system model, firstly, analysis is carried out according to the actual operation condition of the system, and a possible transfer state of the system is modeled to obtain a system state set. Secondly, describing possible transfer rules of the system by using multi-set rewriting, and simulating the transfer rules of the system by using an inference rule representation method to obtain a series of multi-set rewriting rules to form the rewriting rules of the system to form the state transfer rules of the system. Finally, the operation semantics of the system state transition rules are described. And finally, completing the modeling of the concurrent system. Thereby simulating the parallel system state of the multi-party participants of the secure interconnection protocol.
In some embodiments, the protocol deduction rule is modeled as: and describing the message deduction rule of the to-be-verified secure interconnection protocol, wherein the message deduction rule comprises a protocol rule description commonly owned by a protocol participant and the attacker, and a protocol message deduction rule description owned by the attacker but not owned by the protocol participant.
Specifically, in the protocol deduction rule modeling process: the protocol rule description commonly owned by the protocol participant and the attacker comprises: symbol description of specific facts in the security interconnection protocol to be verified and a key rule messaging rule; the protocol message deduction rule description possessed by the attacker but not possessed by the protocol participant comprises: the protocol deduction capability of the attacker receiving the message from the protocol sending party and sending the received message to the protocol receiving party, the protocol deduction capability of the attacker enabling message sending operation to be tracked, the protocol deduction capability of the attacker acquiring the latest system state at any time, the protocol deduction capability of the attacker influencing the system state by tampering the message, and the protocol deduction capability of the attacker performing special processing and deduction on the message.
Specifically, the secure interconnect protocol deduces the rule description. And finishing the message deduction rule description of the specific protocol, wherein the message deduction rule description comprises the protocol rule description commonly owned by the protocol authorization participant and the protocol adversary attacker, and the protocol message deduction rule description of the protocol adversary attacker. Protocol rules, including symbolic descriptions of specific facts to the protocol, key rules, messaging rules, etc., need to be described first. Secondly, we need to describe the adversary protocol deduction rule of the security interconnection protocol, which is a special message deduction rule possessed by an adversary attacker of the protocol, is a capability that an authorized participant does not possess, and is a description of the special capability of the adversary attacker for deducing messages, for example, the attacker is allowed to receive messages from a protocol sending party and send the messages to a protocol receiving party, the message sending operation of the attacker is allowed to be tracked, the attacker is allowed to acquire the latest system state at any time, the attacker is allowed to influence the system state and other capabilities by tampering the messages, and the adversary attacker can perform special processing and deduction the message. The deduction rule description of the specific protocol is realized through the step.
In some embodiments, the protocol trace is described as: and sequencing system actions according to time points to obtain a tracking track, thereby completing protocol tracking description of the to-be-verified security interconnection protocol.
Specifically, in the process of the protocol trace description: and introducing the time point as a protocol tracking attribute to describe a tracking formula, and sequencing each operation completed in the state space search through the time point to describe a semantic process of the tracking formula so as to obtain the tracking track.
In particular, the secure interconnect protocol traces the description. The time point is an attribute value, the protocol message interaction process can be tracked through the attribute, and the system action is sequenced according to the time point, so that the tracking track of the protocol can be obtained. Describing the semantic flow of the tracking formula by various operations completed in the state space search through a time point sequencing method, completing the expansion of a message domain, and obtaining a protocol tracking track.
Fig. 3 is a diagram illustrating an implementation of the TLS1.3 handshake protocol according to an embodiment of the present invention; as shown in fig. 3, describing the handshake process of the TLS1.3 version protocol, first, the user sends a connection request to the server, and after the server receives the request information, after judging that the user is legal, sending response information to inform the user that the server is ready to be connected, after receiving the response information, we introduce the concept of point in time in the above figure, i.e., a, b, c, the execution of each step will be recorded according to the sequence of the occurrence time, forming a part of the protocol trace path, in the figure, the event that the user sends the connection request occurs at the time point a, the server sends the connection response at the time point b, since a < b, the user request event occurs before the server response event in the trace path.
In some embodiments, the preset security attribute of the security interconnection protocol is the security attribute of the security interconnection protocol to be verified, formal verification is performed on the security interconnection protocol to be verified by using a protocol verification tool, when the security interconnection protocol to be verified meets the security attribute of the preset security interconnection protocol, it is determined that no security defect exists, otherwise, attack is positioned according to a counter example.
In particular, secure interconnect protocol security attributes are described. The security attributes that we expect to verify for a protocol are given and described in terms of protocol scenarios. Security attributes include security, Integrity, Authentication. Confidentiality indicates that the information content is confidential if not revealed to an unauthorized entity. Integrity indicates that the information is complete if it has not been modified by any unauthorized entity. Authentication indicates that authorization is granted if the message sender is indeed the original sender and the message is unchanged. After the security attribute is described, the satisfiability will be verified in the subsequent protocol verification process.
Specifically, protocol validation. And inputting the security interconnection protocol model and the security attributes into a verification tool for security interconnection protocol verification. When the protocol is verified, a dependency graph is introduced to represent the execution and causal dependency relationship of the protocol, and verification efficiency is improved. The dependency graph is composed of a rewriting rule instance sequence of the protocol execution process and a protocol operation causal flow. FIG. 4 is a dependency graph introduced at time of protocol validation according to an embodiment of the present invention; as shown in fig. 4, when executing the current Ltk function, the input | Ltk, i.e. the private key, is required and the generation of this parameter depends on the execution of the Register pk function. The introduction of the dependency graph can provide a logic dependency relationship for the verification stage, simplify the search space of the verification stage and improve the verification efficiency.
When the verification tool is used for protocol verification, the protocol model and the protocol security attribute are used as input, the verification tool converts the protocol model and the protocol security attribute into a constraint solving problem, protocol track searching is carried out, whether all tracks of the protocol meet the security attribute or not is analyzed, if the searching is terminated, a protocol track counter-example violating the security attribute is found out, and the counter-example describes a specific attack path, the protocol has security defects. If the search is terminated and no counterexample of the protocol track is found, the protocol is proved to have no security defect. When a counter example is searched, according to time point information introduced in the modeling stage, judgment is carried out after time point sequencing, a path with the counter example is quickly positioned, reasons are analyzed, the false alarm rate of the counter example is reduced, and the verification efficiency is improved.
First embodiment
FIG. 5 is a diagram illustrating formal verification of a secure interconnect protocol according to a first embodiment of the present invention; as shown in fig. 5, the main steps are explained as follows:
1. modeling of encrypted messages: and modeling the encrypted message used by the protocol to obtain an encrypted message model. The modeling method can use the theory of ordered algebra and equation, complete the modeling of the encryption message algorithm (such as encryption, decryption and other steps) by using the sign description of the function algebra sign, and model the attribute of the algorithm by using the theory of equation.
2. Modeling a concurrent system: the concurrent system modeling of the protocol and the opponent model is mainly completed by using multi-set rewriting (namely, symbolizing the form of describing the system state transition rule), and a system model supporting concurrent execution is obtained. Through modeling, a system state set, a system state transition rule and a system state operation semantic are required to be obtained.
3. System state set: and modeling the system state from the actual system condition to obtain a set of the system state.
4. System state transition rules: multiple set rewrites are used to describe possible transition rules for the system. A series of marked multi-set rewrite rules form a marked rewrite system and form system state transition rules. The state transition rule comprises 3 elements of a current state, a transition condition and a next state.
5. System state operation semantics: after describing the state transition rules, the operation semantics of each state transition rule need to be described. Migration rules are conformant grammars, and the operational semantics describe the computational process described by each rule.
6. Modeling protocol deduction rules: modeling the message deduction rule of a specific protocol, wherein the message deduction rule comprises a protocol rule and an opponent protocol deduction rule.
7. Protocol rules: the specific message deduction capability of the protocol is described, and the capability is possessed by protocol participants, wherein the participants comprise authorized participants of the protocol and adversary attackers of the protocol.
8. The adversary agreement deduction rule: the message deduction rule of the protocol opponent attacker can describe the special processing capability of the protocol opponent attacker to the message, and the capability is the capability which is not possessed by the protocol authorization participant.
9. Protocol trace description: by describing the tracking attribute of the time point, the system actions can be sequenced according to the time point to obtain a group of tracking tracks, so that the protocol tracking description is completed.
10. Introducing a time point description tracking formula: the tracking formula is described by introducing the time points as protocol tracking attributes, so that the tracking track of the system protocol can be obtained after the time points are sequenced. This step accurately expresses the protocol tracking description of the previous step by mathematical and logical formulas. And a time point is introduced to obtain a tracking track of the protocol, so that the verification accuracy can be improved. In the verification process, when the counter cases are searched, the judgment is carried out after the time points are sequenced, the problem of errors can be quickly positioned, the false alarm rate of the counter cases is reduced, and the verification efficiency is improved.
11. Secure interconnect protocol model: the establishment of the security interconnection protocol model is completed through encrypted message modeling, concurrent system modeling, protocol deduction rule description and protocol tracking description.
12. Secure interconnect protocol security attributes: the protocol security attributes to be verified are described.
13. Protocol verification: and carrying out protocol verification on the input security interconnection protocol model and security attributes of the security interconnection protocol by using a tool.
14. Secure interconnect protocol results: and analyzing whether the protocol meets the safety attribute or not according to the condition of protocol verification in the last step to obtain the final verification result of the protocol. Finding an attack if finding an counterexample; otherwise, it indicates that the protocol has no security defect.
Second embodiment
Formal verification of the secure interconnect protocol includes the following two parts:
1. modeling secure interconnect protocol
The safety interconnection protocol is used as a network safety protocol for ensuring safety interaction between protocol use main bodies, a multi-party protocol use main body is involved in the protocol use process, and the protocol interaction flow is complex. Aiming at a safety interconnection protocol, firstly modeling is carried out on an encrypted message, then concurrent system modeling is carried out on the protocol, wherein the concurrent system modeling needs to describe a system state set, a system state transition rule and system state operation semantics. And then completing protocol deduction rule modeling, wherein the protocol deduction rule modeling comprises a protocol rule used by the protocol authorized participant and the protocol opponent attacker, and an opponent protocol deduction rule specific to the protocol opponent attacker. And finally, completing protocol tracking description, supporting a protocol tracking process by introducing time points, and obtaining a protocol tracking path by sequencing the time points. The formalized modeling of the security interconnection protocol is completed through the steps, the problem of state space explosion is effectively solved, and the operation condition of the security interconnection protocol can be effectively simulated.
2. Validating portions of a secure interconnect protocol
The verification part, which is already provided with a security interconnection protocol model in the modeling part, needs to provide security attributes of the security interconnection protocol, and automatically searches the state space by using an automatic verification tool capable of performing security protocol symbolic modeling and analysis. If the verification tool gives a counterexample, the protocol is proved to have a security vulnerability. And analyzing to obtain a final verification result of the secure interconnection protocol.
Third embodiment
Fig. 6 is a schematic diagram of a tamarind-driver-based formal verification of a secure interconnect protocol according to a third embodiment of the present invention; as shown in FIG. 6, Tamarin-driver is an advanced tool in the model detection method, firstly performing formal modeling, and then performing formal verification. The method is suitable for various formal verification tools, taking a Tamarin-driver model detection tool as an example, different verification tools adopt different formal description languages and different optimization methods, but the basic principle is based on a state traversal mode, and the method is also suitable.
The first step, modeling is carried out on the encrypted message, and global variables such as an unencrypted text, a private key and a public key are mainly described.
And secondly, describing a concurrent system, mainly declaring communication entities such as Bob, Alice, attackers and the like.
And thirdly, describing protocol deduction rules, wherein the rules describe the capabilities of authorized participants and protocol attackers. Common capabilities such as accepting messages from senders; the attacker capability is the adversary model, which we describe with the Dolev-Yao attack model. Under this model, the attacker has the ability to: any messages that pass through the network can be obtained; is a legitimate user of the network and can therefore initiate a conversation with any other user; the opportunity to become a recipient of any subject sent messages; any other subject can be spoofed to message any subject. The abilities that an attacker does not master are: the random number selected from a sufficiently large space cannot be guessed; without the correct key (or private key), an attacker cannot recover the plaintext from a given ciphertext; for a complete encryption algorithm, an attacker cannot construct the correct ciphertext from a given plaintext; the private part, e.g., the private key that matches a given public key, cannot be solved; while able to control a large public portion of our computing and communication environment, generally he is unable to control many private areas in the computing environment, such as access to memory of offline principals. For the above capability, we describe using multiple set rewrite rules in Tamarin-driver, each indicating a transition from one state S to another state T. All multiple set rewrite rules collectively describe a state migration system. This is a protocol concurrency system model that later proves to be needed.
And fourthly, providing a tracking description of the protocol, namely introducing time points and describing the precedence relationship of each time.
And fifthly, describing the safety attribute of the protocol, and describing the safety attribute by using theorem keywords in the Tamarin-pro. The security attributes are described by first order logic, such as AND or NOR, etc. Including coherence, integrity, authentication. The above security attributes are modeled respectively, and written as an independent theorem, which describes the conditions that need to be satisfied during system state migration, that is, the security properties that the protocol needs to satisfy.
And sixthly, in a formal verification part, inputting a protocol model (including an adversary model) after formal modeling and security attributes into the Tamarin-driver for verification, wherein the verification process belongs to state space traversal. Tamarin-driver uses backward symbol query to prove the property defined by theorem, the backward query means that firstly, if the property is not established, whether an initial state meeting the condition can be obtained from a termination state is observed, if the initial state can be obtained, the existence of a vulnerability is indicated, namely, the security protocol does not meet the property, a counter example is obtained. Conversely, if the initial state cannot be reached, the corresponding properties of the protocol are correct.
The invention discloses a system for formally verifying a secure interconnection protocol in a second aspect. The safety interconnection protocol is a network safety protocol working in a link layer and is used for cooperating with an upper layer control protocol to resist attacks introduced by illegal protocols through main body access. FIG. 7 is a block diagram of a method for formalized validation of a secure interconnect protocol in accordance with an embodiment of the present invention; as shown in fig. 7, the system 700 includes:
a first processing unit 701 configured to: the method comprises the steps of obtaining a to-be-verified security interconnection protocol, and modeling the to-be-verified security interconnection protocol to obtain a security interconnection protocol model, wherein the modeling comprises the following steps: modeling encrypted messages, modeling a concurrent system, modeling protocol deduction rules and describing protocol tracking;
a second processing unit 702 configured to: based on the security interconnection protocol model and the security attributes of a preset security interconnection protocol, executing formal verification of the security interconnection protocol to be verified, and acquiring a verification result;
wherein the first processing unit 701 is specifically configured to:
the encrypted message is modeled as: modeling an encrypted message used in the security interconnection protocol to be verified to acquire an encryption rule, an attribute description and a message value of the encrypted message;
the concurrent system is modeled as: modeling a system state set, a system state transition rule and a system state operation semantic of the to-be-verified security interconnection protocol during concurrence execution so as to simulate concurrence states of a user and an attacker during concurrence execution;
the protocol deduction rule is modeled as follows: describing a message deduction rule of the to-be-verified secure interconnection protocol, wherein the message deduction rule comprises a protocol rule description commonly owned by a protocol participant and the attacker, and a protocol message deduction rule description owned by the attacker but not owned by the protocol participant;
the protocol trace is described as: and sequencing system actions according to time points to obtain a tracking track, thereby completing protocol tracking description of the to-be-verified security interconnection protocol.
According to the system of the second aspect of the invention, in the process of modeling the encrypted message: the encryption rules comprise one or more of encryption algorithm, decryption algorithm, key design rule and random number rule; the attribute description includes: whether information is leaked to an unauthorized entity, whether the information is modified by the unauthorized entity, whether a message sender is an original sender, and whether the sent message is modified; the message values include: public key, private key, encrypted message.
According to the system of the second aspect of the present invention, in the process of modeling the concurrent system, the modeling of the concurrent system is completed by symbolically describing a system state transition rule in a multi-set rewrite manner, which specifically includes:
modeling a to-be-generated transfer state of the system according to the actual running condition of the system so as to obtain the system state set when the concurrency is executed;
describing the system state transition rule by using an inference rule representation method in a multi-set rewriting mode, wherein the system state transition rule comprises a current state, a transition condition and a next state;
describing an operational semantics of the system state transition rule as the system state operational semantics.
According to the system of the second aspect of the present invention, in the protocol deduction rule modeling:
the protocol rule description commonly owned by the protocol participant and the attacker comprises: symbol description of specific facts in the security interconnection protocol to be verified and a key rule messaging rule;
the protocol message deduction rule description possessed by the attacker but not possessed by the protocol participant comprises: the protocol deduction capability of the attacker receiving the message from the protocol sending party and sending the received message to the protocol receiving party, the protocol deduction capability of the attacker enabling message sending operation to be tracked, the protocol deduction capability of the attacker acquiring the latest system state at any time, the protocol deduction capability of the attacker influencing the system state by tampering the message, and the protocol deduction capability of the attacker performing special processing and deduction on the message.
According to the system of the second aspect of the present invention, in the process of the protocol trace description: and introducing the time point as a protocol tracking attribute to describe a tracking formula, and sequencing each operation completed in the state space search through the time point to describe a semantic process of the tracking formula so as to obtain the tracking track.
According to the system of the second aspect of the present invention, the security attribute of the preset secure interconnection protocol is the security attribute of the secure interconnection protocol to be verified, and the second processing unit 702 is specifically configured to: and performing formal verification on the to-be-verified security interconnection protocol by using a protocol verification tool, judging that no security defect exists when the to-be-verified security interconnection protocol meets the security attribute of the preset security interconnection protocol, and otherwise, positioning the attack according to the counter example.
A third aspect of the invention discloses an electronic device. The electronic device comprises a memory and a processor, wherein the memory stores a computer program, and the processor implements the steps of the method for formally verifying the secure interconnection protocol according to any one of the first aspect of the disclosure when executing the computer program.
Fig. 8 is a block diagram of an electronic device according to an embodiment of the present invention, and as shown in fig. 8, the electronic device includes a processor, a memory, a communication interface, a display screen, and an input device, which are connected by a system bus. Wherein the processor of the electronic device is configured to provide computing and control capabilities. The memory of the electronic equipment comprises a nonvolatile storage medium and an internal memory. The non-volatile storage medium stores an operating system and a computer program. The internal memory provides an environment for the operation of an operating system and computer programs in the non-volatile storage medium. The communication interface of the electronic device is used for carrying out wired or wireless communication with an external terminal, and the wireless communication can be realized through WIFI, an operator network, Near Field Communication (NFC) or other technologies. The display screen of the electronic equipment can be a liquid crystal display screen or an electronic ink display screen, and the input device of the electronic equipment can be a touch layer covered on the display screen, a key, a track ball or a touch pad arranged on the shell of the electronic equipment, an external keyboard, a touch pad or a mouse and the like.
It will be understood by those skilled in the art that the structure shown in fig. 8 is only a partial block diagram related to the technical solution of the present disclosure, and does not constitute a limitation of the electronic device to which the solution of the present invention is applied, and a specific electronic device may include more or less components than those shown in the drawings, or combine some components, or have a different arrangement of components.
A fourth aspect of the invention discloses a computer-readable storage medium. The computer readable storage medium has stored thereon a computer program which, when executed by a processor, implements the steps of a method for formal verification of a secure interconnect protocol according to any of the first aspect of the present disclosure.
In conclusion, the technical scheme provided by the invention has high automation degree for verifying the safety interconnection protocol, the protocol parallel condition can be effectively proved, the labor cost is greatly reduced, the user can complete the verification work of the safety protocol without extremely high logical reasoning capability, and the use threshold of a formalized tool is reduced. The complexity of the state space is reduced by applying Pi calculation and other methods, the problem of explosion of the state space is avoided, and the verification speed is improved. Through modeling of the attacker deduction rule, the behavior formalization model of the attacker is described and verified, and the safety of the protocol can be analyzed more completely. The tracking formula is described by introducing the time points as the tracking attributes, so that the tracking track of the protocol can be obtained after the time points are sequenced, the false alarm rate of counter cases is reduced, and the verification efficiency is improved.
The formal verification method provided by the invention has high automation degree for verifying the safety interconnection protocol, the protocol parallel condition can be effectively verified, the labor cost is greatly reduced, the user can complete the verification work of the safety protocol without extremely high logical reasoning capability, and the use threshold of a formal tool is reduced. The complexity of the state space is reduced by applying Pi calculation and other methods, the problem of explosion of the state space is avoided, and the verification speed is improved. The behavior formal model of the attacker is described through modeling of the attacker deduction rule, and verification is carried out, so that the safety of the protocol can be analyzed more completely. The tracking formula is described by introducing the time points as the tracking attributes, so that the tracking track of the protocol can be obtained after the time points are sequenced, the false alarm rate of counter cases is reduced, and the verification efficiency is improved.
Compared with a modal logic method, the modal logic method is simpler and easier to use, but the attack to the protocol cannot be effectively detected. Modal logic in terms of initial assumptions, it is difficult to determine the initial assumptions, if slightly different assumptions are given, an unsafe protocol may be analyzed as a safe protocol, it is difficult to control the idealized scale of the protocol, the protocol needs to be translated into a set of logical formulas, the idealized step itself is not formalized, and its validity and correctness are difficult to guarantee. The logic semantics of modal logic is incomplete, and various attack conditions during protocol parallelism cannot be effectively obtained.
Compared with a theorem proving method, the theorem proving can only verify to obtain a protocol which accords with specific safety properties, the theorem with limited quantity can only prove the defined condition and cannot cover all attacker behaviors, meanwhile, the proving capability has high requirements, the automation degree is low, the proving complexity is high, and the condition when multiple protocols are parallel cannot be well analyzed.
Compared with the traditional test method, the test has the incomplete problem, namely, no method is provided for ensuring all the conditions of the test, and the test method can not meet the verification requirement of a complex system along with the increase of the system scale. Formal verification methods can prove whether the verified security attributes are satisfied and give a conclusion of a counterexample or the absence of a security flaw.
Benefits of Tamarin over other tools for model detection
(1) And the state space is automatically checked, so that the cost is saved. Since the protocol execution may involve a large number of participants, while it is not realistic to manually check the entire state space, while exposing the adversary model, tools like Scyther, proferif, or Tamarin will appear, and after using the tools, we can even find the problem and feedback in time at the protocol design stage.
(2) And a richer built-in library is provided, so that the cost is saved. Tamarin supports various cryptographic primitives and commonly used operations with built-in libraries, wherein the operations include encryption, hashing, signing, exclusive or and the like. He also has built-in library support for DIffie-Hellman theory. This is more scalable than the PROVERIF or Scyther tools.
In addition, in addition to the model detection method, a theorem proving method typified by Isabelle, Coq may be used. The theorem proving method has the main problems of low automation degree and large verification labor input.
It should be noted that the technical features of the above embodiments can be arbitrarily combined, and for the sake of brevity, all possible combinations of the technical features in the above embodiments are not described, however, as long as there is no contradiction between the combinations of the technical features, the scope of the present description should be considered. The above-mentioned embodiments only express several embodiments of the present invention, and the description thereof is more specific and detailed, but not construed as limiting the scope of the invention. It should be noted that, for a person skilled in the art, several variations and modifications can be made without departing from the inventive concept, which falls within the scope of the present invention. Therefore, the protection scope of the present patent should be subject to the appended claims.
Claims (9)
1. A method for formalized verification of a secure interconnection protocol is characterized in that the secure interconnection protocol is a network security protocol working at a link layer and is used for cooperating with an upper control protocol to resist attacks introduced by an illegal protocol through main body access; the method comprises the following steps:
step S1, obtaining a security interconnection protocol to be verified, and modeling the security interconnection protocol to be verified to obtain a security interconnection protocol model, where the modeling includes: modeling encrypted messages, modeling a concurrent system, modeling protocol deduction rules and describing protocol tracking;
step S2, based on the security interconnection protocol model and the security attribute of the preset security interconnection protocol, executing formal verification of the security interconnection protocol to be verified, and acquiring a verification result;
wherein, in the step S1:
the encrypted message is modeled as: modeling an encrypted message used in the to-be-verified security interconnection protocol to acquire an encryption rule, an attribute description and a message value of the encrypted message;
the concurrent system is modeled as: modeling a system state set, a system state transition rule and a system state operation semantic of the to-be-verified security interconnection protocol during concurrent execution so as to simulate concurrent states of a user and an attacker during concurrent execution;
the protocol deduction rule is modeled as follows: describing a message deduction rule of the to-be-verified secure interconnection protocol, wherein the message deduction rule comprises a protocol rule description commonly owned by a protocol participant and the attacker, and a protocol message deduction rule description owned by the attacker but not owned by the protocol participant;
the protocol trace is described as: sequencing system actions according to time points to obtain a tracking track, thereby completing protocol tracking description of the to-be-verified security interconnection protocol;
wherein, in the process of modeling the encrypted message: the encryption rules comprise one or more of encryption algorithm, decryption algorithm, key design rule and random number rule; the attribute description includes: whether information is leaked to an unauthorized entity, whether the information is modified by the unauthorized entity, whether a message sender is an original sender, and whether the sent message is modified; the message values include: public key, private key, encrypted message.
2. The method according to claim 1, wherein during the concurrent system modeling process, the concurrent system modeling is completed by symbolically describing a system state migration rule in a multi-set rewrite manner, and specifically includes:
modeling a to-be-generated transfer state of the system according to the actual running condition of the system so as to obtain the system state set when the concurrency is executed;
describing the system state transition rule by using an inference rule representation method in a multi-set rewriting mode, wherein the system state transition rule comprises a current state, a transition condition and a next state;
and describing the operation semantics of the system state transition rule as the system state operation semantics.
3. The method for formally validating a secure interconnection protocol according to claim 2, wherein in the process of modeling the protocol deduction rule:
the protocol rule description commonly owned by the protocol participant and the attacker comprises: symbol description of specific facts in the security interconnection protocol to be verified and a key rule messaging rule;
the protocol message deduction rule description possessed by the attacker but not possessed by the protocol participant comprises: the protocol deduction capability of the attacker receiving the message from the protocol sending party and sending the received message to the protocol receiving party, the protocol deduction capability of the attacker enabling message sending operation to be tracked, the protocol deduction capability of the attacker acquiring the latest system state at any time, the protocol deduction capability of the attacker influencing the system state by tampering the message, and the protocol deduction capability of the attacker performing special processing and deduction on the message.
4. A method for formally validating a secure interconnect protocol according to claim 3, wherein in the process of the protocol trace description: and introducing the time point as a protocol tracking attribute to describe a tracking formula, and sequencing each operation completed in the state space search through the time point to describe a semantic process of the tracking formula so as to obtain the tracking track.
5. The method according to claim 4, wherein the preset security attributes of the security interconnection protocol are security attributes of the security interconnection protocol to be verified, a protocol verification tool is used for performing formal verification on the security interconnection protocol to be verified, when the security interconnection protocol to be verified meets the security attributes of the preset security interconnection protocol, it is determined that no security defect exists, and otherwise, an attack is positioned according to a counter example.
6. A system for formalized verification of a secure interconnection protocol is characterized in that the secure interconnection protocol is a network security protocol working at a link layer and is used for cooperating with an upper control protocol to resist attacks introduced by illegal protocols through main body access; the system comprises:
a first processing unit configured to: the method comprises the steps of obtaining a security interconnection protocol to be verified, and modeling the security interconnection protocol to be verified to obtain a security interconnection protocol model, wherein the modeling comprises the following steps: modeling encrypted messages, modeling a concurrent system, modeling protocol deduction rules and describing protocol tracking;
a second processing unit configured to: based on the security interconnection protocol model and the security attributes of a preset security interconnection protocol, executing formal verification of the security interconnection protocol to be verified, and acquiring a verification result;
wherein:
the encrypted message is modeled as: modeling an encrypted message used in the to-be-verified security interconnection protocol to acquire an encryption rule, an attribute description and a message value of the encrypted message;
the concurrent system is modeled as: modeling a system state set, a system state transition rule and a system state operation semantic of the to-be-verified security interconnection protocol during concurrence execution so as to simulate concurrence states of a user and an attacker during concurrence execution;
the protocol deduction rule is modeled as follows: describing a message deduction rule of the to-be-verified secure interconnection protocol, wherein the message deduction rule comprises a protocol rule description commonly owned by a protocol participant and the attacker, and a protocol message deduction rule description owned by the attacker but not owned by the protocol participant;
the protocol trace is described as: and sequencing system actions according to time points to obtain a tracking track, thereby completing protocol tracking description of the to-be-verified security interconnection protocol.
7. The system according to claim 6, wherein the security attribute of the predetermined secure interconnect protocol is the security attribute of the secure interconnect protocol to be authenticated, and the second processing unit is specifically configured to: and performing formal verification on the to-be-verified security interconnection protocol by using a protocol verification tool, judging that no security defect exists when the to-be-verified security interconnection protocol meets the security attribute of the preset security interconnection protocol, and otherwise, positioning the attack according to the counter example.
8. An electronic device, comprising a memory storing a computer program and a processor implementing the steps of a method for formal verification of a secure interconnect protocol according to any one of claims 1 to 5 when the computer program is executed by the processor.
9. A computer-readable storage medium, having stored thereon a computer program which, when executed by a processor, carries out the steps of a method of formally validating a secure interconnection protocol as claimed in any one of claims 1 to 5.
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202210402333.1A CN114500347B (en) | 2022-04-18 | 2022-04-18 | Method and system for formalized verification of security interconnection protocol |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202210402333.1A CN114500347B (en) | 2022-04-18 | 2022-04-18 | Method and system for formalized verification of security interconnection protocol |
Publications (2)
| Publication Number | Publication Date |
|---|---|
| CN114500347A CN114500347A (en) | 2022-05-13 |
| CN114500347B true CN114500347B (en) | 2022-06-24 |
Family
ID=81489505
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| CN202210402333.1A Active CN114500347B (en) | 2022-04-18 | 2022-04-18 | Method and system for formalized verification of security interconnection protocol |
Country Status (1)
| Country | Link |
|---|---|
| CN (1) | CN114500347B (en) |
Families Citing this family (2)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN115827494B (en) * | 2023-01-09 | 2023-05-05 | 军事科学院系统工程研究院网络信息研究所 | Design layer form verification method and system |
| CN117041067B (en) * | 2023-07-24 | 2024-10-29 | 中国科学技术大学 | Formalized modeling and verification method and system for block chain underlying protocol |
Citations (4)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US10789404B1 (en) * | 2019-06-06 | 2020-09-29 | Cadence Design Systems, Inc. | System, method, and computer program product for generating a formal verification model |
| CN111756704A (en) * | 2020-05-27 | 2020-10-09 | 西南大学 | A cryptographic protocol authentication method |
| CN112153030A (en) * | 2020-09-15 | 2020-12-29 | 杭州弈鸽科技有限责任公司 | Internet of things protocol security automatic analysis method and system based on formal verification |
| CN113726821A (en) * | 2021-11-02 | 2021-11-30 | 华东交通大学 | Verification method and system for security protocol formalization |
Family Cites Families (1)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US9043746B2 (en) * | 2011-03-07 | 2015-05-26 | International Business Machines Corporation | Conducting verification in event processing applications using formal methods |
-
2022
- 2022-04-18 CN CN202210402333.1A patent/CN114500347B/en active Active
Patent Citations (4)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US10789404B1 (en) * | 2019-06-06 | 2020-09-29 | Cadence Design Systems, Inc. | System, method, and computer program product for generating a formal verification model |
| CN111756704A (en) * | 2020-05-27 | 2020-10-09 | 西南大学 | A cryptographic protocol authentication method |
| CN112153030A (en) * | 2020-09-15 | 2020-12-29 | 杭州弈鸽科技有限责任公司 | Internet of things protocol security automatic analysis method and system based on formal verification |
| CN113726821A (en) * | 2021-11-02 | 2021-11-30 | 华东交通大学 | Verification method and system for security protocol formalization |
Non-Patent Citations (2)
| Title |
|---|
| Formal Verification for SpaceWire Communication Protocol Based on Environment State Machine;Wei Hua等;《IEEE》;20121231;全文 * |
| 计算可靠的密码协议形式化分析综述;雷新锋等;《计算机学报》;20140531;第37卷(第5期);全文 * |
Also Published As
| Publication number | Publication date |
|---|---|
| CN114500347A (en) | 2022-05-13 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| Zhang et al. | Network diversity: a security metric for evaluating the resilience of networks against zero-day attacks | |
| Torroledo et al. | Hunting malicious TLS certificates with deep neural networks | |
| Kobeissi et al. | Verifpal: Cryptographic protocol analysis for the real world | |
| Basin et al. | OFMC: A symbolic model checker for security protocols | |
| Bau et al. | Security modeling and analysis | |
| Chaki et al. | ASPIER: An automated framework for verifying security protocol implementations | |
| CN114500347B (en) | Method and system for formalized verification of security interconnection protocol | |
| Mathew et al. | Integration of blockchain and collaborative intrusion detection for secure data transactions in industrial IoT: a survey | |
| Lugou et al. | Sysml models and model transformation for security | |
| Guo et al. | Model learning and model checking of ipsec implementations for internet of things | |
| Delaune et al. | A theory of dictionary attacks and its complexity | |
| Ameur-Boulifa et al. | Sysml model transformation for safety and security analysis | |
| Lin | Automated analysis of security APIs | |
| Patel et al. | Comparative analysis of formal model checking tools for security protocol verification | |
| US20120304301A1 (en) | Confidentiality analysis support system, method and program | |
| WO2022267184A1 (en) | Blockchain network-based smart contract data security management method and system, and storage medium | |
| Ouffoué et al. | Model-based attack tolerance | |
| Dong et al. | A new method of dynamic network security analysis based on dynamic uncertain causality graph | |
| Nakabayashi et al. | Verification method of key-exchange protocols with a small amount of input using tamarin prover | |
| Braghin et al. | Towards ASM-based automated formal verification of security protocols | |
| CN111639033B (en) | Software security threat analysis method and system | |
| Basagiannis et al. | An intruder model with message inspection for model checking security protocols | |
| Jurjens | Code security analysis of a biometric authentication system using automated theorem provers | |
| Biondi et al. | Security and privacy of protocols and software with formal methods | |
| Ahmadi et al. | On the properties of epistemic and temporal epistemic logics of authentication |
Legal Events
| Date | Code | Title | Description |
|---|---|---|---|
| PB01 | Publication | ||
| PB01 | Publication | ||
| SE01 | Entry into force of request for substantive examination | ||
| SE01 | Entry into force of request for substantive examination | ||
| GR01 | Patent grant | ||
| GR01 | Patent grant |