TY - JOUR

T1 - Semantics for specialising attack trees based on linear logic

AU - Horne, Ross

AU - Mauw, Sjouke

AU - Tiu, Alwen

N1 - Horne, Ross, Mauw, Sjouke, and Tiu, Alwen. ‘Semantics for Specialising Attack Trees Based on Linear Logic’. 1 Jan. 2017 : 57 – 86., DOI: 10.3233/FI-2017-1531
Issue title: Methods for Distributed and Concurrent Systems: Special Issue on the occasion of the 60th Birthday of Professor Gabriel Ciobanu

PY - 2017/6/7

Y1 - 2017/6/7

N2 - Attack trees profile the sub-goals of the proponent of an attack. Attack trees have a variety of semantics depending on the kind of question posed about the attack, where questions are captured by an attribute domain. We observe that one of the most general semantics for attack trees, the multiset semantics, coincides with a semantics expressed using linear logic propositions. The semantics can be used to compare attack trees to determine whether one attack tree is a specialisation of another attack tree. Building on these observations, we propose two new semantics for an extension of attack trees named causal attack trees. Such attack trees are extended with an operator capturing the causal order of sub-goals in an attack. These two semantics extend the multiset semantics to sets of series-parallel graphs closed under certain graph homomorphisms, where each semantics respects a class of attribute domains. We define a sound logical system with respect to each of these semantics, by using a recently introduced extension of linear logic, called MAV, featuring a non-commutative operator. The non-commutative operator models causal dependencies in causal attack trees. Similarly to linear logic for attack trees, implication defines a decidable preorder for specialising causal attack trees that soundly respects a class of attribute domains.

AB - Attack trees profile the sub-goals of the proponent of an attack. Attack trees have a variety of semantics depending on the kind of question posed about the attack, where questions are captured by an attribute domain. We observe that one of the most general semantics for attack trees, the multiset semantics, coincides with a semantics expressed using linear logic propositions. The semantics can be used to compare attack trees to determine whether one attack tree is a specialisation of another attack tree. Building on these observations, we propose two new semantics for an extension of attack trees named causal attack trees. Such attack trees are extended with an operator capturing the causal order of sub-goals in an attack. These two semantics extend the multiset semantics to sets of series-parallel graphs closed under certain graph homomorphisms, where each semantics respects a class of attribute domains. We define a sound logical system with respect to each of these semantics, by using a recently introduced extension of linear logic, called MAV, featuring a non-commutative operator. The non-commutative operator models causal dependencies in causal attack trees. Similarly to linear logic for attack trees, implication defines a decidable preorder for specialising causal attack trees that soundly respects a class of attribute domains.

KW - attack trees

KW - semantics

KW - causality

KW - linear logic

KW - calculus of structures

U2 - 10.3233/FI-2017-1531

DO - 10.3233/FI-2017-1531

M3 - Article

SN - 0169-2968

VL - 153

SP - 57

EP - 86

JO - Fundamenta Informaticae

JF - Fundamenta Informaticae

IS - 1-2

ER -