Computer Science ›› 2018, Vol. 45 ›› Issue (2): 209-214.doi: 10.11896/j.issn.1002-137X.2018.02.036

Previous Articles     Next Articles

Modeling for Three Kinds of Network Attacks Based on Temporal Logic

NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang   

  • Online:2018-02-15 Published:2018-11-13

Abstract: Compared with other detection methods,the intrusion detection methods based on temporal logic can detect many complex network attacks effectively.There is no network attack temporal logic formula,so common back,ProcessTable and Saint attacks can not be detected using the above method.Thus,this paper employed propositional interval temporal logic (ITL) and real-time attack signature logic (RASL) to model the temporal logic formula for the three attacks,respectively.In general,based on attack basic principle of the three attacks,the key attack steps are decomposed into atomic actions.Next,this paper defined atomic propositions.Lastly,according to the relationship between the atomicpropositions,this paper constructed the network attack temporal logic formula which is an input of the model checker.In addition,the automaton was used to model the log library as another input of the model checker.The output of the model checker is the result of intrusion detection in the three network attacks.Besides,the intrusion detection method for three attacks was given.

Key words: Propositional interval temporal logic,Real-time attack signature logic,Model checking,Intrusion detection

[1] RPGER M,GOUBAULT-LARRECQ J.Log Auditing through Model-Checking [C]∥IEEE Workshop on Computer Security Foundations.2001:220-234.
[2] SUN Y,WU T Y,MA X Q,et al.Modeling and verifying EPC network intrusion system based on timed automata[J].Pervasive and Mobile Computing,2016,24(C):61-67.
[3] CHAKIR E M,KHAMLICHI Y I, MOUGHIT M.Handling alerts for intrusion detection system using stateful pattern matching[C]∥IEEE 4th International Colloquium on Information Science and Technology.2017:139-144.
[4] CLARKE E M,GRUNBERG O,PELED D A.Model Checking [M].MIT Press Cambridge,MA,USA,1997:54-56.
[5] RAMPURE V,TIWARI A.A rough set based feature selection on KDD CUP 99 data set[J].International Journal of Database Theory and Application,2015,8(1):149-156.
[6] CHEN X Y.Research on Network Attack Model Based onTemporal Logic [D].Zhengzhou:Zhengzhou University,2014.(in Chinese) 陈茜月.基于时序逻辑的网络攻击建模研究[D].郑州:郑州大学,2014.
[7] HU W.Modeling and Detection of Network Attack Based onTemporal Logic [D].Zhengzhou:Zhengzhou University,2015.(in Chinese) 胡伟.基于时序逻辑的网络攻击建模与检测[D].郑州:郑州大学,2015.
[8] XU P T.Intrusion Detection Based On Model Checking Benchmark Test Platform For Research [D].Zhengzhou:Zhengzhou University,2016.(in Chinese) 许鹏涛.基于模型检测的入侵检测基准测试平台研究[D].郑州:郑州大学,2016.
[9] ZHU W J,WANG Z Y,ZHANG H B.A novel algorithm for Intrusion Detection based on Model Checking Interval Temporal Logic [J].China Communications,2011,8(3):66-72.(in Chinese) 朱维军,王忠勇,张海滨.一种基于区间时序逻辑模型检测的入侵检测算法[J].中国通信,2011,8(3):66-72.
[10] DUAN Z H,TIAN C,ZHANG L.A decision procedure forpropositional projection temporal logic with infinite models [J].Acta Informatica,2008,45(1):43-78.
[11] TIAN C,DUAN Z H.Complexity of propositional projectiontemporal logic with star [J].Mathematical Structures in Computer Science,2009,9(1):73-100.
[12] ZHU W J.Model Checking Timed Interval Temporal Logic:Theory,Algorithms and Application[D].Xi’an:Xidian University,2011.(in Chinese) 朱维军.时间区间时序逻辑模型检测:理论、算法及应用[D].西安:西安电子科技大学,2011.
[13] ZHU W J,ZHOU Q L,YANG W D,et al.A Novel Algorithm for Intrusion Detection Based on RASL Model Checking [J].Mathematical Problems in Engineering,2013,2013(3):1-10.(in Chinese) 朱维军,周清雷,杨卫东,等.一种基于实时攻击签名逻辑模型检测的入侵检测算法[J].工程中的数学问题,2013,2013(3):1-10.
[14] ZHU W J,ZHANG H B,ZHOU Q L.On the Decidability of Satisfiability of Discrete TITL formulae[J].Acta Electronica Sinica,2010,38(5):1039-1045.(in Chinese) 朱维军,张海滨,周清雷.离散时间区间时序逻辑可满足性的判定[J].电子学报,2010,38(5):1039-1045.
[15] SOLANKAR P,PINGALE S.International Journal of Computer Science and Information Technologies[J].International Journal of Computer Science and Information Technologies(IJCSIT),2015,6(2):1096-1099.

No related articles found!
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75 .
[2] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[3] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[4] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[5] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99 .
[6] ZHOU Yan-ping and YE Qiao-lin. L1-norm Distance Based Least Squares Twin Support Vector Machine[J]. Computer Science, 2018, 45(4): 100 -105 .
[7] LIU Bo-yi, TANG Xiang-yan and CHENG Jie-ren. Recognition Method for Corn Borer Based on Templates Matching in Muliple Growth Periods[J]. Computer Science, 2018, 45(4): 106 -111 .
[8] GENG Hai-jun, SHI Xin-gang, WANG Zhi-liang, YIN Xia and YIN Shao-ping. Energy-efficient Intra-domain Routing Algorithm Based on Directed Acyclic Graph[J]. Computer Science, 2018, 45(4): 112 -116 .
[9] CUI Qiong, LI Jian-hua, WANG Hong and NAN Ming-li. Resilience Analysis Model of Networked Command Information System Based on Node Repairability[J]. Computer Science, 2018, 45(4): 117 -121 .
[10] WANG Zhen-chao, HOU Huan-huan and LIAN Rui. Path Optimization Scheme for Restraining Degree of Disorder in CMT[J]. Computer Science, 2018, 45(4): 122 -125 .