Semantics for Specialising Attack Trees based on Linear Logic
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 s...
Saved in:
Main Authors: | , , |
---|---|
Other Authors: | |
Format: | Article |
Language: | English |
Published: |
2017
|
Subjects: | |
Online Access: | https://hdl.handle.net/10356/83503 http://hdl.handle.net/10220/42718 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Nanyang Technological University |
Language: | English |
id |
sg-ntu-dr.10356-83503 |
---|---|
record_format |
dspace |
spelling |
sg-ntu-dr.10356-835032020-03-07T11:48:52Z Semantics for Specialising Attack Trees based on Linear Logic Horne, Ross Mauw, Sjouke Tiu, Alwen School of Computer Science and Engineering Semantics Attack trees 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. NRF (Natl Research Foundation, S’pore) MOE (Min. of Education, S’pore) Accepted version 2017-06-16T04:23:06Z 2019-12-06T15:24:23Z 2017-06-16T04:23:06Z 2019-12-06T15:24:23Z 2016 Journal Article Horne, R., Mauw, S., & Tiu, A. (2017). Semantics for Specialising Attack Trees based on Linear Logic. Fundamenta Informaticae, 153(1-2), 57-86. 0169-2968 https://hdl.handle.net/10356/83503 http://hdl.handle.net/10220/42718 10.3233/FI-2017-1531 en Fundamenta Informaticae © 2016 IOS Press and the authors. This is the author created version of a work that has been peer reviewed and accepted for publication by Fundamenta Informaticae, IOS Press and the authors. It incorporates referee’s comments but changes resulting from the publishing process, such as copyediting, structural formatting, may not be reflected in this document. The published version is available at: [https://dx.doi.org/10.3233/FI-2017-1531]. 26 p. application/pdf |
institution |
Nanyang Technological University |
building |
NTU Library |
country |
Singapore |
collection |
DR-NTU |
language |
English |
topic |
Semantics Attack trees |
spellingShingle |
Semantics Attack trees Horne, Ross Mauw, Sjouke Tiu, Alwen Semantics for Specialising Attack Trees based on Linear Logic |
description |
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. |
author2 |
School of Computer Science and Engineering |
author_facet |
School of Computer Science and Engineering Horne, Ross Mauw, Sjouke Tiu, Alwen |
format |
Article |
author |
Horne, Ross Mauw, Sjouke Tiu, Alwen |
author_sort |
Horne, Ross |
title |
Semantics for Specialising Attack Trees based on Linear Logic |
title_short |
Semantics for Specialising Attack Trees based on Linear Logic |
title_full |
Semantics for Specialising Attack Trees based on Linear Logic |
title_fullStr |
Semantics for Specialising Attack Trees based on Linear Logic |
title_full_unstemmed |
Semantics for Specialising Attack Trees based on Linear Logic |
title_sort |
semantics for specialising attack trees based on linear logic |
publishDate |
2017 |
url |
https://hdl.handle.net/10356/83503 http://hdl.handle.net/10220/42718 |
_version_ |
1681040352476135424 |