Abstract: The intrusion detection method based on model checking of projection temporal logic can describe piecewise network attacks but concurrent attacks. We defined a novel concurrent operation and obtained a new intrusion detection method based on model checking of concurrent propositional projection temporal logic. I3y example, we show that our method can detect concurrent attacks efficiently.

Key words: Intrusion detection, Misuse detection, Model checking, Concurrent propositional projection temporal logic