Research On Network Attack Model Based On Temporal Logic

With the types of network attacks getting more and more diverse, thetechnology of attacks getting more and more complex, the intrusion detectiontechnology becoming more and more important. Intrusion detection is an importantnetwork security technology. Depending on the detection principle, it can beclassified as misuse detection and anomaly detection. Due to the high false rate ofanomaly detection, the intrusion detection systems international community hasdeployed mostly use misuse detection methods. However, faced with the growingnetwork, there are a lot of complex changes, the technique based on pattern matchingseriously lacks of capacity. In this regard, method based on model checking ispresented.Compared with the intrusion detection based on pattern matching, the intrusiondetection method based on model checking can effectively enhance the ability todetect changes in complex attacks. However, concerning of the current intrusiondetection method based on model checking, there are still several issues to beresolved.First, although there are similar methods specific to one or several certain typesof attacks of modeling, it still lacks of the model designed for the general process ofattacks. Secondly, it lacks of a platform who can provide a basis for comparing theperformance of similar methods. These are the two issues that this thesis will studyon.1. Giving out the definition of a general process of network attacks, and basedon this formula we define a network attack model, and finally refine the modelestablished formula, so that we get the general model of network attacks based on theinterval temporal logic. The new model can cover the general process of networkattacks. The intrusion detection on the basis of the new model will help to put on theimplementation of intrusion detection model based intrusion detection technology tothe full common type of attack detection.2. On the basis of the study on39kinds of four categories attacks in KDD dataset, we get detailed analysis of the principles of various types of attacks, thenconvert the specific details of each attack into the corresponding action sequences thathave been recorded in the log file. Each attack will eventually be described astemporal logic formulas, as an input to the model of the detector, to detect intrusions.Thus13attacks were constructed and laid the foundation of the comparison of theperformance of similar methods, and to provide a technical framework for therealization of high ability to detect the type of attacks.Thesis is an important part of the National Natural Science Foundation of theUnited Fund Project (U1204608) and China Postdoctoral Science Foundation fundedproject(2012M511588).