@MASTERSTHESIS\{IMM2012-06398, author = "T. S. Lind{\o}", title = "Policy Invalidation in System Models", year = "2012", school = "Technical University of Denmark, {DTU} Informatics, {E-}mail: reception@imm.dtu.dk", address = "Asmussens Alle, Building 305, {DK-}2800 Kgs. Lyngby, Denmark", type = "", note = "Supervised by Associate Professor Christian Probst, probst@imm.dtu.dk, {DTU} Informatics.", url = "http://www.imm.dtu.dk/English.aspxTo", abstract = "We live in a world becoming increasingly complex, and it is equally difficult to ensure safety and security in such systems, especially against insiders. Formalising and analysing these systems can prove beneficial in order to specify or verify any threats or vulnerabilities. In this project, we formalise real-world systems and subsequently perform static analysis to investigate these systems, and check whether they can invalidate any pre-defined system policies. The results show us that policy invalidation, based on static analysis, is useful on the battleground of modern security measures, as it can help to discover vulnerabilities and threats when designing or improving systems. Multiple extensions can yield a more life-like system-modelling tool, increasing both functionality and quality of the threat assessment." }