An Intuitionistic Linear Logical Semantics of SAND Attack Trees

TL;DR

This paper develops a new logical framework called Attack Tree Linear Logic (ATLL) for modeling SAND attack trees, providing a formal foundation based on intuitionistic linear logic and advanced semantic models.

Contribution

It introduces ATLL, a novel logic for attack trees, with semantics based on lineales and dialectica models, supporting full distributivity of sequential conjunction.

Findings

ATLL provides a formal semantics for SAND attack trees.

The semantics are based on lineales and dialectica models.

ATLL supports full distributivity of sequential conjunction over choice.

Abstract

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.