Attack-Defence Trees (ADTs) are well-suited to assess possible attacks to systems and the eﬃciency of counter-measures. In this paper, we ﬁrst enrich the available constructs with reactive patterns that cover further security scenarios, and equip all constructs with attributes such as time and cost to allow quantitative analyses. Then, ADTs are modelled as (an extension of) Asynchronous Multi-Agents Systems— EAMAS. The ADT–EAMAS transformation is performed in a systematic manner that ensures correctness. The transformation allows us to quantify the impact of diﬀerent agents conﬁgurations on metrics such as attack time. Using EAMAS also permits parametric veriﬁcation: we derive constraints for property satisfaction. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools.
|Number of pages||19|
|Publication status||Published - 2019|