Deciding the Non-emptiness of Attack Trees

  • Maxime Audinot
  • Sophie PinchinatEmail author
  • François Schwarzentruber
  • Florence Wacheux
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11086)


We define and study the decision problem of the non-emptiness of an attack tree. This decision problem reflects the natural question of knowing whether some attack scenario described by the tree can be realized in (a given model of) the system to defend. We establish accurate complexity bounds, ranging from Open image in new window -completeness for arbitrary trees down to Open image in new window -completeness for trees with no occurrence of the AND operator. Additionally, if the input system to defend has a succinct description, the non-emptiness problem becomes Open image in new window -complete.


  1. 1.
    Aslanyan, Z., Nielson, F.: Model checking exact cost for attack scenarios. In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 210–231. Springer, Heidelberg (2017). Scholar
  2. 2.
    Audinot, M., Pinchinat, S., Kordy, B.: Is my attack tree correct? In: Foley, S.N., Gollmann, D., Snekkenes, E. (eds.) ESORICS 2017. LNCS, vol. 10492, pp. 83–102. Springer, Cham (2017). Scholar
  3. 3.
    Audinot, M., Pinchinat, S., Kordy, B.: Guided design of attack trees: a system-based approach - to be published. In: 31th IEEE Computer Security Foundations Symposium, CSF 2018. IEEE (2018)Google Scholar
  4. 4.
    Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825–885. IOS Press, Amsterdam (2009)Google Scholar
  5. 5.
    Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRefGoogle Scholar
  6. 6.
    Bylander, T.: The computational complexity of propositional STRIPS planning. Artif. Intell. 69(1–2), 165–204 (1994)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151–158. ACM (1971)Google Scholar
  8. 8.
    Horne, R., Mauw, S., Tiu, A.: Semantics for specialising attack trees based on linear logic. Fundam. Inform. 153(1–2), 57–86 (2017)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Ivanova, M.G., Probst, C.W., Hansen, R.R., Kammüller, F.: Attack tree generation by policy invalidation. In: Akram, R.N., Jajodia, S. (eds.) WISTP 2015. LNCS, vol. 9311, pp. 249–259. Springer, Cham (2015). Scholar
  10. 10.
    Ivanova, M.G., Probst, C.W., Hansen, R.R., Kammüller, F.: Transforming graphical system models to graphical attack models. In: Mauw, S., Kordy, B., Jajodia, S. (eds.) GraMSec 2015. LNCS, vol. 9390, pp. 82–96. Springer, Cham (2016). Scholar
  11. 11.
    Jhawar, R., Kordy, B., Mauw, S., Radomirović, S., Trujillo-Rasua, R.: Attack trees with sequential conjunction. In: Federrath, H., Gollmann, D. (eds.) SEC 2015. IAICT, vol. 455, pp. 339–353. Springer, Cham (2015). Scholar
  12. 12.
    Kumar, R., Ruijters, E., Stoelinga, M.: Quantitative attack tree analysis via priced timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 156–171. Springer, Cham (2015). Scholar
  13. 13.
    Lindell, S.: A logspace algorithm for tree canonization (extended abstract). In: Proceedings of the 24th Annual ACM Symposium on Theory of Computing, Victoria, British Columbia, Canada, 4–6 May 1992, pp. 400–404 (1992)Google Scholar
  14. 14.
    Mauw, S., Oostdijk, M.: Foundations of attack trees. In: Won, D.H., Kim, S. (eds.) ICISC 2005. LNCS, vol. 3935, pp. 186–198. Springer, Heidelberg (2006). Scholar
  15. 15.
    Nielson, H.R., Nielson, F., Vigo, R.: Discovering, quantifying, and displaying attacks. Log. Meth. Comput. Sci. 12 (2016)Google Scholar
  16. 16.
    Papadimitriou, C.H.: Computational Complexity. Academic Internet Publ., Ventura (2007)zbMATHGoogle Scholar
  17. 17.
    Pinchinat, S., Acher, M., Vojtisek, D.: Towards synthesis of attack trees for supporting computer-aided risk analysis. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 363–375. Springer, Cham (2015). Scholar
  18. 18.
    Pinchinat, S., Acher, M., Vojtisek, D.: ATSyRa: an integrated environment for synthesizing attack trees. In: Mauw, S., Kordy, B., Jajodia, S. (eds.) GraMSec 2015. LNCS, vol. 9390, pp. 97–101. Springer, Cham (2016). Scholar
  19. 19.
    Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177–192 (1970)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Schneier, B.: Attack trees: modeling security threats. Dr. Dobb’s J. Softw. Tools 24(12), 21–29 (1999)Google Scholar
  21. 21.
    Sipser, M.: Introduction to the Theory of Computation. PWS Publishing Company, Boston (1997)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Maxime Audinot
    • 1
  • Sophie Pinchinat
    • 1
    Email author
  • François Schwarzentruber
    • 1
    • 2
  • Florence Wacheux
    • 1
  1. 1.Univ. Rennes, IRISA, CNRSRennesFrance
  2. 2.ENS RennesRennesFrance

Personalised recommendations