Intrusion Detection for Universal Attack Mode Based on Linear Temporal Logic with Past Construct

Compared with the intrusion detection based on pattern matching, the method which is based on model checking can detect the complex attacks. But all of the existing algorithms are only used to detect some specific types of attacks. To solve this problem, we firstly use the Linear Temporal Logic with Past Construct (LTLPC) formulae to set up formal sub-models for the five kinds of attackers, the four kinds of attack processes and the eight kinds of attack effects. According to their universal relationship and the semantic relation of variety of LTLPC operators, we obtain the above sub-models together, thus, the universal models described by LTLPC formulae for universal attacks are formed. On this base, we implement an intrusion detection method based on LTLPC for detecting all types of attacks. Compared with the existing methods, the detecting ability of the new method is more comprehensive.