Analysis of Attack Time and Costs in Attack Trees via SMT Resolution
Aliyu Tanko Ali, Damas P. Gruska, Karam Kharraz, Martin Leucker · 2024
Attack trees are a visual formalism used to model potential vulnerabilities and demonstrate how an asset or target might be compromised.Many attacks are feasible only within specific time constraints, where vulnerabilities become accessible during limited time windows.In this paper, we extend traditional attack trees by incorporating time constraints at non-leaf nodes to represent when an attack can succeed, while associating leaf nodes with attack costs and durations.We translate our model into the Z3 SMT solver to verify attack traces and determine minimal-cost attack paths that adhere to these time constraints.Practical applications of this approach include improving security risk assessments and optimizing decision-making in time-sensitive environments.