Benchmark tests for the model-checking-based ids algorithms

Miaolei Deng, Heling Cao, Weijun Zhu, Huanmei Wu, Yangyue Zhou

Research output: Contribution to journalArticle

1 Scopus citations


A fundamental concern for the security community is to identify the comprehensive comparable performance of various intrusion detection algorithms which are based on the Model Checking (MC) techniques. To address this open issue, we conduct the benchmark tests for the model-checking-based intrusion detection systems algorithms. At first, linear temporal logic, interval temporal logic and real-time attack signature logic are employed respectively to establish formula models for twenty-four types of attacks selected from KDDCUP, i.e., the annual data mining and knowledge discovery competition organized by association for computing machinery. And then, a standard intrusion set, called intrusion set for intrusion detection based on model checking, which is a behavior version of a subset of KDDCUP, is constructed. On the basis of it, detection abilities and efficiency of the intrusion detection algorithms based on model checking the three logics mentioned above are compared exhaustively. The experimental results illustrate the efficiency and abilities of these three algorithms. It is beneficial for selecting the suitable MC-based algorithms in actual deployment of intrusion detection systems.

Original languageEnglish (US)
Article number8822670
Pages (from-to)135479-135498
Number of pages20
JournalIEEE Access
StatePublished - Jan 1 2019


  • Benchmark test
  • Intrusion detection systems
  • Model checking
  • Network security
  • Temporal logic

ASJC Scopus subject areas

  • Computer Science(all)
  • Materials Science(all)
  • Engineering(all)

Fingerprint Dive into the research topics of 'Benchmark tests for the model-checking-based ids algorithms'. Together they form a unique fingerprint.

  • Cite this