Attack-Defense Trees (ADTs) are widely used for modeling dynamic interactions between a potential system attacker and the system’s defender. They offer a structured and intuitive approach to quantitative analysis, enabling the identification of threats and the evaluation of defense strategies using various attributes. However, many existing approaches to ADT analysis suffer from a significant limitation—the restricted expressiveness of the models, which hinders in-depth analysis of ADTs. This creates a scientific gap in the field of cybersecurity and system analysis. This thesis aims to address this gap by developing a novel generative tool that au
tomates the creation of ADT models into PRISM code for formal verification. The tool will support both tree-structured and DAG-structured ADTs with cost metrics. Using this tool, it will be possible to conduct in-depth analysis of the trees, identify potential vulnerabilities, and model hypothetical scenarios for their prevention.