Vulnerability analysis of networks to detect multiphase attacks using the actor-based language Rebeca

Shahriari HR, Jalili R. Using CSP to model and analyze transmission control vulnerabilities within the broadcast network. In: Proceedings of IEEE international networking and communication conference (INCC’2004); June 2004. p. 42–7. Zakeri R, Shahriari HR, Jalili R, Sadoddin R. Modeling TCP/IP networks topology for network vulnerability analysis. In: Proceedings of 2nd international symposium of telecommunications (IST2005); September 10–12. 2005. p. 653–8. Shahriari HR, Sadoddin R, Jalili R, Zakeri R, Omidian AR. Network vulnerability analysis through vulnerability take-grant model (VTG), In: Proceedings of 7th international conference on information and communications security (ICICS2005), LNCS, vol. 3783; 2005. p. 256–8. Ramakrishnan, 2002, Model based analysis of configuration vulnerabilities, J Comput Security, 10, 189, 10.3233/JCS-2002-101-209 Ryan, 2001 Rohrmair G, Lowe G. Using CSP to detect insertion and evasion possibilities within the intrusion detection area. In: Proceedings of BCS workshop on formal aspects of security; 2002. Rohrmair, 2005, Using data-independence in the analysis of intrusion detection systems, Theor Comput Sci, 340, 82, 10.1016/j.tcs.2005.03.004 Jajodia, 2003, Topological analysis of network attack vulnerability Noel S, Robertson E, Jajodia S. Correlating intrusion events and building attack scenarios through attack graph distances. In: Proceedings of the 20th annual computer security applications conference. Tucson, Arizona; December 2004. p. 350–9. Ryan, 2001 Zerkle D, Levitt K. NetKuang – a multihost configuration vulnerability checker. In: Proceedings of the sixth USENIX UNIX security symposium. San Jose, CA; 1996. p. 195–204. Dacier M, Deswarte Y. Privilege graph: an extension to the typed access matrix model. In: Proceedings of third european symposium on research in computer security (ESORICS 94), Lecture notes in computer science, vol. 875. Brighton, UK: Springer-Verlag; 1994. p. 319–34. Ritchey RW, Ammann P. Using model checking to analyze network vulnerabilities. In: Proceedings of IEEE symposium on security and privacy; May 2001. p. 156–65. Sirjani M, Movaghar A. An actor-based model for formal modeling of reactive systems: Rebeca. Technical Report CS-TR-80-01. Tehran, Iran; 2001. Sirjani, 2004, Modeling and verification of reactive systems using Rebeca, Fundamenta Informaticae, 63, 385 Sirjani M, Movaghar A, Mousavi M. Compositional verification of an object-based reactive system. In: Proceedings of the workshop on automated verification of critical systems (AVoCS’01). Oxford, UK; 2001. p. 114–8. SMV. SMV: A Symbolic Model Checker. Available from: <http://www.cs.cmu.edu/modelcheck/>. Sheyner O, Haines J, Jha S, Lippmann R, Wing J. Automated generation and analysis of attack graphs. In: Proceedings of IEEE symposium on security and privacy; 2002. p. 273–84. Bellovin, 1989, Security problems in the TCP/IP protocol suite, Comput Commun Rev, 19, 32, 10.1145/378444.378449 Hewitt C. Description and theoretical analysis (using schemata) of PLANNER: a language for proving theorems and manipulating models in a robot. PhD Thesis, MIT; 1971. Agha, 1990 Agha, 1997, A foundation for actor computation, J Funct Program, 7, 1, 10.1017/S095679689700261X Sirjani M, Movaghar A, Iravanchi H, Jaghoori M, Shali A. Model checking in Rebeca. In: Proceedings of parallel and distributed processing techniques and applications (PDPTA’03); June 2003. p. 1819–22. Sirjani, 2005, Model checking, automated abstraction, and compositional verification of Rebeca models, J Universal Comput Sci, 11, 1054 Sirjani M, Shali A, Jaghouri MM, Iravanchi H, Movaghar A. A front-end tool for automated abstraction and modular verification of actor-based models. In: Proceedings of fourth international conference on application of concurrency to system design (ACSD)2004. Hamilton, Canada: IEEE Computer Society; June 2004. p. 145–8. Jaghoori M, Movaghar A, Sirjani M. Modere: the model checking engine of Rebeca. In: Proceedings of ACM symposium on applied computing – software verification track; 2006. p. 1810–5. Jaghoori M, Sirjani M, Mousavi MR, Movaghar A. Efficient symmetry reduction for an actor-based model. In: Proceedings of 2nd international conference on distributed computing and internet technology. Lecture notes in computer science, vol. 3816; 2005. p. 494–507. Derasion R. [online] The Nessus attack scripting language reference guide; 2000. Available from: <http://www.nessus.org>. Internet Security Systems. [online] System scanner information. Available from: <http://www.iss.net>. Network Associates. [online] CyberCop Scanner Information. Available from: <http://www.nai.com/asp_set/products/tns/ccscanner_intro.asp>. Spin Model Checker. [online] Available from: <http://netlib.bell-labs.com/netlib/spin>. Undercoffer J, Pinkston J. Modeling computer attacks: a target-centric ontology for intrusion detection. In: Proceedings of 2002 CADIP research symposium; 2005. Bishop, 2003 Shahriari, 2007, Vulnerability take-grant (VTG): an efficient approach to analyze network vulnerabilities, Comput Security, 25, 349, 10.1016/j.cose.2007.03.002