  In this paper we introduce a new logical foundation of SAND attack trees in
intuitionistic linear logic. This new foundation is based on a new logic called
the Attack Tree Linear Logic (ATLL). Before introducing ATLL we given several
new logical models of attack trees, the first, is a very basic model based in
truth tables. Then we lift this semantics into a semantics of attack trees
based on lineales which introduces implication, but this can be further lifted
into a dialectica model which ATLL is based. One important feature of ATLL is
that it supports full distributivity of sequential conjunction over choice.
