Modeling And Detection Of Network Attack Based On Temporal Logic

With the normalization, diversification and variation of network attacks, intrusion detection technology is getting more and more attentions. Intrusion detection technology can be divided misuse detection and anomaly detection according to the different detection principles, anomaly detection, however due to the presence of natural defects in its high rate of false positives, so the international community has achieved most of the use of intrusion detection system based on pattern matching misuse detection technology. However, with the expansion as well as attacks on the increasingly complex network data, based on pattern matching techniques to detect capacity is clearly insufficient, therefore, model-based intrusion detection techniques have been proposed.Compared with traditional intrusion detection technology, model-based intrusion detection technology can detect complex changes in types of attacks, however, this detection method is still a number of problems need to be studied. Firstly, the lack of modeling studies and related performance comparison of specific types of attacks. Secondly, the lack of change more complicated types of attacks to establish common attack model. In this paper, the main work is as follows:1.11 kinds of common attack types KDD CUP dataset attacked principle analysis, action sequences deduced atomic details of each attack under attack attack, on this basis, to obtain a collection of atomic formulas each attack, and according to movement behavior of all types of attacks to establish a time interval temporal logic formulas. The simulation results show that the new method of detecting ability.2. This paper proposed Universal Types Attack Detection (UTA) based on Concurrent Proposition Concurrent Propositional Projection Temporal Logic (CPPTL). Use CPPTL of five attackers, eight attack effect, five attack tools established formal description of the formula to obtain the general equation of Universal types of attacks. Through the common model equations and data sets model checking algorithm experimental results show that the new method can cover a wider detection range and the ability to detect changes in Universal types of complex network attacks.Thesis is an important part of the National Natural Science Foundation of the United Fund Project (U1204608) and China Postdoctoral Science Foundation funded project(2012M511588) and China Postdoctoral Science Foundation funded project (2015M572120).