A journal of IEEE and CAA , publishes high-quality papers in English on original theoretical/experimental research and development in all areas of automation
Advanced Search
Volume 5 Issue 1
Jan.  2018

IEEE/CAA Journal of Automatica Sinica

  • JCR Impact Factor: 15.3, Top 1 (SCI Q1)
    CiteScore: 23.5, Top 2% (Q1)
    Google Scholar h5-index: 77， TOP 5
Turn off MathJax
Article Contents
Article Navigation >  IEEE/CAA Journal of Automatica Sinica  > 2018  >  5(1): 92-107
Weijun Zhu, Miaolei Deng and Qinglei Zhou, "An Intrusion Detection Algorithm for Wireless Networks Based on ASDL," IEEE/CAA J. Autom. Sinica, vol. 5, no. 1, pp. 92-107, Jan. 2018. doi: 10.1109/JAS.2017.7510754
Citation: Weijun Zhu, Miaolei Deng and Qinglei Zhou, "An Intrusion Detection Algorithm for Wireless Networks Based on ASDL," IEEE/CAA J. Autom. Sinica, vol. 5, no. 1, pp. 92-107, Jan. 2018. doi: 10.1109/JAS.2017.7510754
shu

An Intrusion Detection Algorithm for Wireless Networks Based on ASDL

doi: 10.1109/JAS.2017.7510754
  • 1.

    School of Information Engineering, Zhengzhou University, Zhengzhou 450001, China

  • 2.

    College of Information Science and Engineering, Henan University of Technology, Zhengzhou 450001, China

Funds:

the National Natural Science Foundation of China U1204608

the National Natural Science Foundation of China U1304606

the National Natural Science Foundation of China 61572444

the Postdoctoral Science Foundation of China 2012M511588

the Postdoctoral Science Foundation of China 2015M572120

the National Key R & D Plan of China 2016YFB0800100

the Science Foundation for Young Key Teachers at the Universities of Henan Province 2014GGJS-001

the Science and Technology Development Project of Henan Province 152102410033

More Information
    Abstract
  • Wireless networks are more vulnerable to cyberattacks than cable networks. Compared with the misuse intrusion detection techniques based on pattern matching, the techniques based on model checking (MC) have a series of comparative advantages. However, the temporal logics employed in the existing latter techniques cannot express conveniently the complex attacks with synchronization phenomenon. To address this problem, we formalize a novel temporal logic language called attack signature description language (ASDL). On the basis of it, we put forward an ASDL model checking algorithm. Furthermore, we use ASDL programs, which can be considered as temporal logic formulas, to describe attack signatures, and employ other ASDL programs to create an audit log. As a result, the ASDL model checking algorithm can be presented for automatically verifying whether or not the latter programs satisfy the formulas, that is, whether or not the audit log coincides with the attack signatures. Thus, an intrusion detection algorithm based on ASDL is obtained. The case studies and simulations show that the new method can find coordinated chop-chop attacks.

     

    • FullText(HTML)
  • loading
    • References(35)
  • [1]
    M. Roger and J. Goubault-Larrecq, "Log auditing through modelchecking, " in Proc. 14th IEEE Workshop on Computer Security Foundations, Washington, DC, USA, 2001, pp. 220-234. http://ieeexplore.ieee.org/document/930148/
    [2]
    W. J. Zhu, Z. Y. Wang, and H. B. Zhang, "Intrusion detection algorithm based on model checking interval temporal logic, " China Commun., vol. 8, no. 3, pp. 66-72, May 2011. http://en.cnki.com.cn/Article_en/CJFDTotal-ZGTO201103010.htm
    [3]
    E. M. Clarke, O. Grumberg, and D. Peled, Model Checking. Cambridge, Massachusetts, London, England:The MIT Press, 1999.
    [4]
    J. Olivain and J. Goubault-Larrecq, "The ORCHIDS intrusion detection tool, " in Proc. 17th Int. Conf. Computer Aided Verification, Edinburgh, Scotland, UK, 2005, pp. 286-290. doi: 10.1007/11513988_28
    [5]
    W. J. Zhu, Q. L. Zhou, W. D. Yang, and H. B. Zhang, "A novel algorithm for intrusion detection based on RASL model checking, " Math. Probl. Eng., vol. 2013, pp. Article ID 621203, Feb. 2013. http://www.oalib.com/paper/2320548
    [6]
    E. Nowicka and M. Zawada, "Modeling temporal properties of multievent attack signatures in interval temporal logic, "[Online]. Available: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.100.488&rep=rep1&type=pdf. 2006.
    [7]
    C. V. Zhou, C. Leckie, and S. Karunasekera, "A survey of coordinated attacks and collaborative intrusion detection, " Comput. Secur., vol. 29, no. 1, pp. 124-140, Feb. 2010. http://www.sciencedirect.com/science/article/pii/S016740480900073X
    [8]
    F. B. Cohen, "A note on distributed coordinated attacks, " Comput. Secur., vol. 15, no. 2, pp. 103-121, Dec. 1996. http://www.sciencedirect.com/science/article/pii/0167404896893230
    [9]
    J. Goubault-Larrecq and J. Olivain, "A smell of orchids, " in Proc. 8th Int. Workshop, RV 2008, Budapest, Hungary, 2008, pp. 1-20. 10.1007/978-3-540-89247-2_1
    [10]
    R. Ben Younes, G. Tremblay, and G. Bégin, "Extending orchids for intrusion detection in 802. 11 wireless networks, " in Proc. 8th Int. Conf. New Technologies in Distributed Systems, New York, NY, USA, 2008, pp. Article ID 8. https://dl.acm.org/citation.cfm?id=1416740
    [11]
    Y. Zhang, J. M. Fu, and X. M. Sun, "A method of intrusion detection based on model-checking, " J. Wuhan Univ. Nat. Sci. Ed., vol. 51, no. 3, pp. 319-322, Jun. 2005. http://en.cnki.com.cn/Article_en/CJFDTOTAL-WHDY200503015.htm
    [12]
    M. Q. Ali and E. Al-Shaer, "Probabilistic model checking for AMI intrusion detection, " in Proc. 2013 IEEE Int. Conf. Smart Grid Communications (SmartGridComm), Vancouver, BC, Canada, 2013, pp. 468-473. http://ieeexplore.ieee.org/document/6688002/
    [13]
    A. M. Ahmed, "Online network intrusion detection system using temporal logic and stream data processing, " Ph. D. dissertation, Univ. of Liverpool, Liverpool, UK, 2013. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.579415
    [14]
    T. Jacob, M. Raman, and S. Singh, "Intrusion detection in zero knowledge system using model checking approach, " in Computer Networks & Communications (NetCom), N. Chaki, N. Meghanathan, and D. Nagamalai, Eds. New York, NY, USA: Springer, 2013, pp. 453-465. doi: 10.1007/978-1-4614-6154-8_45
    [15]
    A. Sinha, A. Ry, and S. Singh, "Modeling & verification of sliding window protocol with data loss and intruder detection using NuSMV, " in Proc. 2nd Int. Conf. Computational Science, Engineering and Information Technology, Coimbatore, India, 2012, pp. 352-357. https://dl.acm.org/citation.cfm?id=2393276
    [16]
    B. Moszkowski, "Reasoning about digital circuits, " Ph. D. dissertation, Depart. Comput. Sci., Stanford Univ., Stanford, USA, 1983. https://dl.acm.org/citation.cfm?id=911281
    [17]
    Z. H. Duan, Modeling and Analysis of Hybrid Systems. Beijing, China:Science Press, 2004.
    [18]
    W. J. Zhu, H. B. Zhang, and Q. L. Zhou, "On the decidability of satisfiability of discrete TITL formulae, " Acta Electron. Sinica, vol. 38, no. 5, pp. 1039-1045, May 2010. http://en.cnki.com.cn/Article_en/CJFDTOTAL-DZXU201005010.htm
    [19]
    C. C. Zhou, C. A. R. Hoare, and A. P. Ravn, "A calculus of durations, " Inf. Process. Lett., vol. 40, no. 5, pp. 269-276, Dec. 1991. http://www.ams.org/mathscinet-getitem?mr=1148468
    [20]
    M. G. Ouyang, F. Pan, and Y. T. Zhang, "ISITL: Intrusion signatures in augmented interval temporal logic, " in Proc. Int. Conf. Machine Learning and Cybernetics, Xi'an, China, vol. 3, pp. 1630-1635, 2003. http://ieeexplore.ieee.org/document/1259757/
    [21]
    M. G. Ouyang and Y. B. Zhou, "ISDTM: An intrusion signatures description temporal model, " Wuhan Univ. J. Nat. Sci., vol. 8, no. 2, pp. 373-378, Jun. 2003. http://kns.cnki.net/KCMS/detail/detail.aspx?filename=whdz200302008&dbname=CJFD&dbcode=CJFQ
    [22]
    P. Beaucamps, I. Gnaedig, and J. Y. Marion, "Abstraction-based malware analysis using rewriting and model checking, " in Proc. 17th European Symp. Research in Computer Security, Pisa, Italy, 2012, pp. 806-823. doi: 10.1007/978-3-642-33167-1_46
    [23]
    J. Kinder, S. Katzenbeisser, C. Schallhart, and H. Veith, "Proactive detection of computer worms using model checking, " IEEE Trans. Depend. Secure Comput., vol. 7, no. 4, pp. 424-438, Oct. -Dec. 2010. http://ieeexplore.ieee.org/document/4689469/
    [24]
    F. Song and T. Touili, "LTL model-checking for malware detection, " in Proc. 19th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy, 2013, pp. 416-431. https://dl.acm.org/citation.cfm?id=2450430
    [25]
    F. Song and T. Touili, "Efficient malware detection using modelchecking, " in Proc. 18th Int. Symp. Formal Methods, Paris, France, 2012, pp. 418-433. doi: 10.1007/978-3-642-32759-9_34
    [26]
    F. Song and T. Touili, "Model-checking for android malware detection, " in Proc. 12th Asian Symp. Programming Languages and Systems, Singapore, 2014, pp. 216-235. doi: 10.1007/978-3-319-12736-1_12
    [27]
    F. Song and T. Touili, "Pushdown model checking for malware detection, " Int. J. Softw. Tools Technol. Transf., vol. 16, no. 2, pp. 147-173, Apr. 2014. doi: 10.1007/978-3-642-28756-5_9
    [28]
    S. Schmerl, M. Vogel, and H. König, "Using model checking to identify errors in intrusion detection signatures, " Int. J. Softw. Tools Technol. Transf., vol. 13, no. 1, pp. 89-106, Jan. 2011. doi: 10.1007/s10009-010-0166-6
    [29]
    Y. Sun, T. Y. Wu, X. Q. Ma, and H. C. Chao, "Modeling and verifying EPC network intrusion system based on timed automata, " Perv. Mobile Comput., vol. 24, pp. 61-76, Dec. 2015. http://www.sciencedirect.com/science/article/pii/S1574119215001145
    [30]
    N. Ellouze, S. Rekhis, M. Allouche, and N. Boudriga, "Digital investigation of security attacks on cardiac implantable medical devices, " Electron. Proc. Theor. Comput. Sci., vol. 165, pp. 15-30, Oct. 2014. http://www.oalib.com/paper/4047899
    [31]
    Z. H. Duan, C. Tian, and L. Zhang, "A decision procedure for propositional projection temporal logic with infinite models, " Acta Inf., vol. 45, no. 1, pp. 43-78, Feb. 2008. doi: 10.1007/s00236-007-0062-z
    [32]
    C. Tian and Z. H. Duan, "Complexity of propositional projection temporal logic with star, " Math. Struct. Comput. Sci., vol. 19, no. 1, pp. 73-100, Feb. 2009. http://www.sciencedirect.com/science/article/pii/S0304397510007486
    [33]
    C. Tian and Z. H. Duan, "Expressiveness of propositional projection temporal logic with star, " Theor. Comput. Sci., vol. 412, no. 18, pp. 1729-1744, Apr. 2011. http://www.sciencedirect.com/science/article/pii/S0304397510007486
    [34]
    Z. H. Duan, Temporal Logic and Temporal Logic Programming. Beijing:Science Press, 2005.
    [35]
    X. B. Wang, "Object-oriented MSVL and its application to verification of composite web services, " Ph. D. dissertation, Univ. of Xidian, Xi'an, China, 2009. http://cdmd.cnki.com.cn/Article/CDMD-10701-2009195303.htm
    • Related Articles
    • Supplements(0)

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Figures(13)  / Tables(8)

    Get Citation
    PDF
    XML

    Article Metrics

    Article views (1428) PDF downloads(65) Cited by()

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return