IEEE/CAA Journal of Automatica Sinica
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. 92107, Jan. 2018. doi: 10.1109/JAS.2017.7510754 
[1] 
M. Roger and J. GoubaultLarrecq, "Log auditing through modelchecking, " in Proc. 14th IEEE Workshop on Computer Security Foundations, Washington, DC, USA, 2001, pp. 220234. 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. 6672, May 2011. http://en.cnki.com.cn/Article_en/CJFDTotalZGTO201103010.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. GoubaultLarrecq, "The ORCHIDS intrusion detection tool, " in Proc. 17th Int. Conf. Computer Aided Verification, Edinburgh, Scotland, UK, 2005, pp. 286290. 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. 124140, 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. 103121, Dec. 1996. http://www.sciencedirect.com/science/article/pii/0167404896893230

[9] 
J. GoubaultLarrecq and J. Olivain, "A smell of orchids, " in Proc. 8th Int. Workshop, RV 2008, Budapest, Hungary, 2008, pp. 120. 10.1007/9783540892472_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 modelchecking, " J. Wuhan Univ. Nat. Sci. Ed., vol. 51, no. 3, pp. 319322, Jun. 2005. http://en.cnki.com.cn/Article_en/CJFDTOTALWHDY200503015.htm

[12] 
M. Q. Ali and E. AlShaer, "Probabilistic model checking for AMI intrusion detection, " in Proc. 2013 IEEE Int. Conf. Smart Grid Communications (SmartGridComm), Vancouver, BC, Canada, 2013, pp. 468473. 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. 453465. doi: 10.1007/9781461461548_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. 352357. 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. 10391045, May 2010. http://en.cnki.com.cn/Article_en/CJFDTOTALDZXU201005010.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. 269276, Dec. 1991. http://www.ams.org/mathscinetgetitem?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. 16301635, 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. 373378, 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, "Abstractionbased malware analysis using rewriting and model checking, " in Proc. 17th European Symp. Research in Computer Security, Pisa, Italy, 2012, pp. 806823. doi: 10.1007/9783642331671_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. 424438, Oct. Dec. 2010. http://ieeexplore.ieee.org/document/4689469/

[24] 
F. Song and T. Touili, "LTL modelchecking for malware detection, " in Proc. 19th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy, 2013, pp. 416431. 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. 418433. doi: 10.1007/9783642327599_34

[26] 
F. Song and T. Touili, "Modelchecking for android malware detection, " in Proc. 12th Asian Symp. Programming Languages and Systems, Singapore, 2014, pp. 216235. doi: 10.1007/9783319127361_12

[27] 
F. Song and T. Touili, "Pushdown model checking for malware detection, " Int. J. Softw. Tools Technol. Transf., vol. 16, no. 2, pp. 147173, Apr. 2014. doi: 10.1007/9783642287565_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. 89106, Jan. 2011. doi: 10.1007/s1000901001666

[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. 6176, 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. 1530, 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. 4378, Feb. 2008. doi: 10.1007/s002360070062z

[32] 
C. Tian and Z. H. Duan, "Complexity of propositional projection temporal logic with star, " Math. Struct. Comput. Sci., vol. 19, no. 1, pp. 73100, 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. 17291744, 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, "Objectoriented 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/CDMD107012009195303.htm
