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

Abstract:

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 used to detect some specific types of attacks. So, we firstly use the Interval Temporal Logic with Past Construct (ITLPC) formulae to set up formal sub-models respectively 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 ITLPC logic operators, we obtain the above sub-models together, thus, the universal models described by ITLPC formulae for universal attacks are formed. On this base, we implement an intrusion detection method based on ITLPC for detecting all types of attacks. Compared with the existing methods, the detecting ability of the new method is more comprehensive.

• Periodical: Advanced Materials Research (Volumes 1006-1007)
• Pages: 1047-1050
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.1006-1007.1047
• Online since: August 2014
• Authors: Yong Liang Li, Wei Jun Zhu, Qing Lei Zhou
• Keywords: Interval Temporal Logic with Past Construct, Intrusion Detection, Model Checking

References

[1] M Roger, J Goubault-Larrecq, Log Auditing through Model-Checking, in Proceedings of the 14th IEEE workshop on Computer Security Foundations, IEEE Computer Society  Washington, DC, USA, 2001, pp.220-234.

DOI: 10.1109/csfw.2001.930148

[2] J Olivain, J Goubault-Larrecq, The Orchids Intrusion Detection Tool, in Proceedings of the 17th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, 3576: 286-290, Springer, Edinburgh, Scotland, UK, (2005).

DOI: 10.1007/11513988_28

[3] J Goubault-Larrecq , J Olivain, A Smell of Orchids, in Runtime Verification: 8th International Workshop, Budapest, Hungary, March 30, 2008, pp.1-20.

DOI: 10.1007/978-3-540-89247-2_1

[4] W Zhu, Z Wang, H Zhang, A novel algorithm for Intrusion Detection based on Model Checking Interval Temporal Logic, China Communications, Vol. 8, Issue 3, 2011, pp.66-72.

[5] WeiJun Zhu, YiRan Wang, QingLei Zhou, An intrusion detection method based on modeling checking of projection temporal logic, Network security technology and application, Vol. 3, 2010, pp.25-27.

[6] W Zhu, Q Zhou, W Yang, et al, A Novel Algorithm for Intrusion Detection Based on RASL Model Checking, mathematical problems in engineering, vol. 2013, Article ID 621203, 10 pages, 2013. DOI: 10. 1155/2013/621203.

DOI: 10.1155/2013/621203

[7] W Zhu, Intrusion detection based on model checking timed interval temporal logic，in IEEE International Conference on Information Theory and Information Security, IEEE press, Beijing, 2010, pp.503-505.

DOI: 10.1109/icitis.2010.5689549

[8] H Liu，Principle and Implementation of Computer Network Security，BeiJing：Machinery Industry Press, 2009 (in Chinese).

[9] Z Duan, C Tian, L Zhang， A decision procedure for propositional projection temporal logic with infinite models, Acta Informatica, Vol. 45, Issue 1, 2008, pp.43-78.

DOI: 10.1007/s00236-007-0062-z