Semantics for Specialising Attack Trees based on Linear Logic

• Autorzy: Horne R. , Mauw S. , Tiu A.

Identyfikatory

DOI

10.3233/FI-2017-1531

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

attack trees; calculus of structures; causality; linear logic; semantics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 153, nr 1/2
• Strony: 57--86
• Opis fizyczny: Bibliogr. 20 poz., rys.

Twórcy

autor

Horne R.

• School of Computer Science and Engineering, Nanyang Technological University, Singapore

autor

Mauw S.

• CSC/SnT, University of Luxembourg, Luxembourg

autor

Tiu A.

• School of Computer Science and Engineering, Nanyang Technological University, Singapore

Bibliografia

• [1] Schneier B. Attack trees. Dr. Dobb’s journal, 1999;24(12):21–29.
• [2] Jhawar R, Kordy B, Mauw S, Radomirović S, Trujillo-Rasua R. Attack trees with sequential conjunction. In: Proc. IFIPSec’15, volume 455 of IFIP AICT. 2015 pp. 339–353. doi:10.1007/978-3-319-18467-8_23.
• [3] Mauw S, Oostdijk M. Foundations of attack trees. In: Proc. ICISC’05, volume 3935 of LNCS. 2006 pp. 186–198. doi:10.1007/11734727_17.
• [4] Rehák M, et al. Runtime Monitoring and Dynamic Reconfiguration for Intrusion Detection Systems. In: Proc. RAID’09, volume 5758 of LNCS. 2009 pp. 61–80. doi:10.1007/978-3-642-04342-0_4.
• [5] Kordy B, Kordy P, Mauw S, Schweitzer P. ADTool: Security Analysis with Attack-Defense Trees. In: Proc. QEST’13, volume 8054 of LNCS, pp. 173–176. 2013. doi:10.1007/978-3-642-40196-1_15.
• [6] Girard JY. Linear logic. Theoretical computer science, 1987;50(1):1–101. URL https://doi.org/10.1016/0304-3975(87)90045-4.
• [7] Guglielmi A. A system of interaction and structure. ACM Transactions on Computational Logic, 2007; 8(1):1. doi:10.1145/1182613.1182614.
• [8] Horne R. The Consistency and Complexity of Multiplicative Additive System Virtual. Scientific Annals of Computer Science, 2015;25(2):245–316. doi:10.7561/SACS.2015.2.245.
• [9] Jürgenson A, Willemson J. Serial Model for Attack Tree Computations. In: Proc. ICISC’09, volume 5984 of LNCS. 2009 pp. 118–128. doi: 10.1007/978-3-642-14423-3_9.
• [10] Andreoli JM. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 1992;2(3):297–347. URL https://doi.org/10.1093/logcom/2.3.297.
• [11] Kordy B, Mauw S, Schweitzer P. Quantitative questions on Attack-Defense Trees. In: Proc. ICISC’12, volume 7839 of LNCS. 2013 pp. 49–64. doi:10.1007/978-3-642-37682-5_5.
• [12] Valdes J, Tarjan RE, Lawler EL. The recognition of series parallel digraphs. In: Proc. STOC’79. ACM, 1979 pp. 1–12. doi:10.1145/800135.804393.
• [13] Gischer JL. The equational theory of pomsets. Theor Comput Sci, 1988;61(2-3):199–224. doi:10.1016/0304-3975(88)90124-7.
• [14] Ciobanu G, Horne R. A provenance tracking model for data updates. In: Proc. FOCLASA’12, volume 91 of EPTCS. 2012 pp. 31–44. doi:10.4204/EPTCS.91.3.
• [15] Van Glabbeek R, Goltz U. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 2001;37(4-5):229–327. doi:10.1007/s002360000041.
• [16] Kordy B, Mauw S, Radomirović S, Schweitzer P. Attack-Defense trees. Journal of Logic and Computation, 2014;24(1):55–87. URL https://doi.org/10.1093/logcom/exs029.
• [17] Aslanyan Z, Nielson F, Parker D. Quantitative Verification and Synthesis of Attack-Defence Scenarios. In: CSF’16. IEEE. ISBN 978-1-5090-2607-4, 2016 pp. 105–119.
• [18] Cheney J, Ahmed A, Acar UA. Provenance as dependency analysis. Mathematical Structures in Computer Science, 2011;21(6):1301–1337. URL https://doi.org/10.1017/S0960129511000211.
• [19] Cheney J, Chiticariu L, Tan WC. Provenance in Databases: Why, How, and Where. Foundations and Trends in Databases, 2009;1(4):379–474. doi:10.1561/1900000006.
• [20] Green TJ, Karvounarakis G, Tannen V. Provenance semirings. In: Proc. PODS’07. ACM, 2007 pp. 31–40. doi:10.1145/1265530.1265535.