Research On Intrusion Detection Methods Based On The Temporal Logic Model Validation

Most of the current intrusion detection systems use pattern matching algorithmto detect intrusion in the world. With the increase of the amount of data on theinternet, these systems are faced with some difficult problems. So some formalmethods are raised and be applied to the intrusion detection system. The methodbased on Proposition Linear Temporal Logic (PLTL) is one of the representatives, andhas been proven that it can been used to detect complex attacks which can change.However, it is still not clear what the advantages and the disadvantages are comparedwith other related methods. This is the problem we must solve at soon. This papermainly includes two parts:(1)The pattern matching algorithm(MPA) and the intrusion detection algorithmbased on the model checking (MCA) are analyzed in detail in the field of misusedetection technology. And I carry out the simulation experiment to compare theirdetection capability and efficiency on the basis of KDD99dataset.(2) The paper propose a detection method for universal attack based onProjection Temporal Logic (PTL). This method sets up form sub-models for attacker,attack effect and attack process, then gets them together using PTL, so we get thePTL formula model for universal attack. The experiment results show that the newmethod has more comprehensive detecting ability.The above researches work get some preliminary conclusions about theperformance of the intrusion detection algorithm, which provide a reference for choiceto use algorithm in practical.