TY - GEN
T1 - On linear logic, functional programming, and attack trees
AU - Eades, Harley
AU - Jiang, Jiaming
AU - Bryant, Aubrey
N1 - Funding Information:
Acknowledgments. This work was supported by NSF award #1565557. We thank Clément Aubert for helpful discussions and feedback on previous drafts of this paper, and the anonymous reviewers whose recommendations made this a better paper.
Publisher Copyright:
© 2019, Springer Nature Switzerland AG.
PY - 2019
Y1 - 2019
N2 - This paper has two main contributions. The first is a new linear logical semantics of causal attack trees in four-valued truth tables. Our semantics is very simple and expressive, supporting specializations, and supports the ideal semantics of causal attack trees, and partially supporting the filter semantics of causal attack trees. Our second contribution is Lina, a new embedded, in Haskell, domain specific functional programming language for conducting threat analysis using attack trees. Lina has many benefits over existing tools; for example, Lina allows one to specify attack trees very abstractly, which provides the ability to develop libraries of attack trees, furthermore, Lina is compositional, allowing one to break down complex attack trees into smaller ones that can be reasoned about and analyzed incrementally. Furthermore, Lina supports automatically proving properties of attack trees, such as equivalences and specializations, using Maude and the semantics introduced in this paper.
AB - This paper has two main contributions. The first is a new linear logical semantics of causal attack trees in four-valued truth tables. Our semantics is very simple and expressive, supporting specializations, and supports the ideal semantics of causal attack trees, and partially supporting the filter semantics of causal attack trees. Our second contribution is Lina, a new embedded, in Haskell, domain specific functional programming language for conducting threat analysis using attack trees. Lina has many benefits over existing tools; for example, Lina allows one to specify attack trees very abstractly, which provides the ability to develop libraries of attack trees, furthermore, Lina is compositional, allowing one to break down complex attack trees into smaller ones that can be reasoned about and analyzed incrementally. Furthermore, Lina supports automatically proving properties of attack trees, such as equivalences and specializations, using Maude and the semantics introduced in this paper.
UR - http://www.scopus.com/inward/record.url?scp=85064691812&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85064691812&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-15465-3_5
DO - 10.1007/978-3-030-15465-3_5
M3 - Conference contribution
AN - SCOPUS:85064691812
SN - 9783030154646
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 71
EP - 89
BT - Graphical Models for Security - 5th International Workshop, GraMSec 2018, Revised Selected Papers
A2 - Pym, David
A2 - Cybenko, George
A2 - Fila, Barbara
PB - Springer Verlag
T2 - 5th International Workshop on Graphical Models for Security, GraMSec 2018
Y2 - 8 July 2018 through 8 July 2018
ER -