Automated Synthesis of Enforcing Mechanisms for Security Properties in a Timed Setting 1

In [Martinelli, F. and I. Matteucci, Modeling security automata with process algebras and related results (2006), presented at the 6th International Workshop on Issues in the Theory of Security (WITS '06) - Informal proceedings; Martinelli, F. and I. Matteucci, Through modeling to synthesis of security automata (2006), accepted to STM06. To appeare in ENTCS] we have presented an approach for enforcing security properties. It is based on the automatic synthesis of controller programs that are able to detect and eventually prevent possible wrong action performed by an external agent. Here, we extend this approach also to a timed setting. Under certain assumptions, we are also able to enforce several information flow properties. We show how to deal with parameterized systems.