ADT2AMAS

I contributed to the design of a transformation model from Attack-Defense Trees (ADT) to Asynchronous Multi-Agent Systems (AMAS) that preserves given conditions.

In security issues is necessary to evaluate the chances of attacks being successful with regard to the counter measures that could be proposed. An attack-defense system is characterized by the order of executions and the time required by each individual operation and its cost. In particular, the best defense at the lowest cost are sought. ADTs enjoy a graphical representation, allowing for an easy understanding of the structure of the model, and a semantics for their formal analysis.

However, the formalism of the ADT does not have sufficient expressiveness to apply verification techniques to the computational system, so within the research an automatic translation was proposed to another approach that does, Asynchronous MultiAgent Systems (AMAS). This last formalism offers a succinct representation in which reachability properties can be easily verified.

The support of this work was established in the design and implementation of the ADT and AMAS formalisms as well as an automatic translator that given an ADT returns an equivalent AMAS that respects a given set of rules. I implemented such transformation in C++ under the supervision of Jaime Arias and Laure Petrucci during 3 months from September 2018 to December 2018.