A Logical Framework for Evaluating Network Resilience Against Faults and Attacks

  • Elie Bursztein
  • Jean Goubault-Larrecq
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4846)


We present a logic-based framework to evaluate the resilience of computer networks in the face of incidents, i.e., attacks from malicious intruders as well as random faults. Our model uses a two-layered presentation of dependencies between files and services, and of timed games to represent not just incidents, but also the dynamic responses from administrators and their respective delays. We demonstrate that a variant TATL\(\Diamond\) of timed alternating-time temporal logic is a convenient language to express several desirable properties of networks, including several forms of survivability. We illustrate this on a simple redundant Web service architecture, and show that checking such timed games against the so-called TATL\(\Diamond\) variant of the timed alternating time temporal logic TATL is EXPTIME-complete.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Artz, M.: NetSPA : a Network Security Planning Architecture. PhD thesis, Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science (2002)Google Scholar
  3. 3.
    Balthrop, J., Forrest, S., Newman, M.E.J., Williamson, M.M.: Technological networks and the spread of computer viruses. science 304(23) (2004)Google Scholar
  4. 4.
    Brihaye, T., Henzinger, T.A., Raskin, J., Prabhu, V.: Minimum-time reachability in timed games. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, Springer, Heidelberg (2006)Google Scholar
  5. 5.
    Church, A.: logic, arithmetics and automata. In: Congress of Mathematician, Institut Mittag-Leffler, pp. 23–35 (1962)Google Scholar
  6. 6.
    Colizza, V., Barrat, A., Barthelemy, M., Vespignani, A.: The modeling of global epidemics: stochastic dynamics and predictability. Bulletin of Mathematical Biology 68, 1893–1921 (2006)CrossRefMathSciNetGoogle Scholar
  7. 7.
    de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, Springer, Heidelberg (2003)Google Scholar
  8. 8.
    du net, J.: Bouygues telecom privé de réseau (2004)Google Scholar
  9. 9.
    Henzinger, T., Prabhu, V.: Timed alternating-time temporal logic. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 1–18. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    ICANN. Dns attack factsheet. Technical report, ICANN (March 2007)Google Scholar
  11. 11.
    Jajodia, S.: Topological analysis of network attack vulnerability. In: ASIACCS 2007. Proceedings of the 2nd ACM symposium on Information, computer and communications security, Singapore, p. 2. ACM Press, New York (2007)CrossRefGoogle Scholar
  12. 12.
    Jha, S., Sheyner, O., Wing, J.: Two formal analysis of attack graphs. In: CSFW 2002. Proceedings of the 15th IEEE Computer Security Foundations Workshop, Washington, DC, USA, p. 49. IEEE Computer Society Press, Los Alamitos (2002)Google Scholar
  13. 13.
    Klensin, J.: Rfc 2821 - simple mail transfer protocol. Technical report, IETF Network Working Group (2001)Google Scholar
  14. 14.
    Lippmann, R., Webster, S., Stetson, D.: The effect of identifying vulnerabilities and patching software on the utility of network intrusion detection. In: Wespi, A., Vigna, G., Deri, L. (eds.) RAID 2002. LNCS, vol. 2516, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  15. 15.
    Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (extended abstract). In: STACS 1995, pp. 229–242 (1995)Google Scholar
  16. 16.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989. Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Austin, Texas, United States, pp. 179–190. ACM Press, New York (1989)CrossRefGoogle Scholar
  17. 17.
    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, p. 156. IEEE Computer Society Press, Los Alamitos (2000)Google Scholar
  18. 18.
    Saffre, F., Halloy, J., Deneubourg, J.L.: The ecology of the grid. In: ICAC 2005. Proceedings of the Second International Conference on Automatic Computing, Washington, DC, USA, pp. 378–379. IEEE Computer Society Press, Los Alamitos (2005)Google Scholar
  19. 19.
    Schneier, B.: Attack trees: Modeling security threats. Dr. Dobb?s journal (December 1999)Google Scholar
  20. 20.
    Schneier, B.: Secrets & Lies: Digital Security in a Networked World. Wiley, Chichester (2000)Google Scholar
  21. 21.
    Williamson, M.M.: Throttling viruses: Restricting propagation to defeat malicious mobile code. acsac 00: 61 (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Elie Bursztein
    • 1
  • Jean Goubault-Larrecq
    • 1
  1. 1.LSV, ENS Cachan, CNRS, INRIA 

Personalised recommendations