Abstract
NetQi is a freely available model-checker designed to analyze network incidents such as intrusion. This tool is an implementation of the anticipation game framework, a variant of timed game tailored for network analysis. The main purpose of NetQi is to find, given a network initial state and a set of rules, the best strategy that fulfills player objectives by model-checking the anticipation game and comparing the outcome of each play that fulfills strategy constraints. For instance, it can be used to find the best patching strategy. NetQi has been successfully used to analyze service failure due to hardware, network intrusion, worms and multiple-site intrusion defense cooperation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: Time for playing games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007)
Bursztein, E.: Netqi, http://www.netqi.org
Bursztein, E.: Network administrator and intruder strategies. Technical Report LSV-08-02, LSV, ENS Cachan (January 2008)
Bursztein, E., Goubault-Larrecq, J.: A logical framework for evaluating network resilience against faults and attacks. In: 12th annual Asian Computing Science Conference (ASIAN), December 2007, pp. 212–227. Springer, Heidelberg (2007)
de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 144–158. Springer, Heidelberg (2003)
Ramakrishan, C., Sekar, R.: Model-based analysis of configuration vulnerabilities. Journal of Computer Security 1, 198–209 (2002)
Ritchey, R.W., Ammann, P.: Using model checking to analyze network vulnerabilities. In: SP 2000: Proceedings of the 2000 IEEE Symposium on Security and Privacy, Washington, DC, USA, pp. 156–165. IEEE Computer Society Press, Los Alamitos (2000)
Sheyner, O., Haines, J., Jha, S., Lippmann, R., Wing, J.M.: Automated generation and analysis of attack graphs. In: SP 2002: Proceedings of the 2002 IEEE Symposium on Security and Privacy, Washington, DC, USA, pp. 273–284. IEEE Computer Society Press, Los Alamitos (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bursztein, E. (2008). NetQi: A Model Checker for Anticipation Game. In: Cha, S.(., Choi, JY., Kim, M., Lee, I., Viswanathan, M. (eds) Automated Technology for Verification and Analysis. ATVA 2008. Lecture Notes in Computer Science, vol 5311. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88387-6_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-88387-6_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88386-9
Online ISBN: 978-3-540-88387-6
eBook Packages: Computer ScienceComputer Science (R0)