Invalidating policies using structural information

Florian Kammüller, Christian W. Probst

    Research output: Contribution to journalArticleAcademicpeer-review

    3 Citations (Scopus)
    113 Downloads (Pure)


    Insider threats are a major threat to many organisations. Even worse, insider attacks are usually hard to detect, especially if an attack is based on actions that the attacker has the right to perform. In this paper we present a step towards detecting the risk for this kind of attacks by invalidating policies using structural information of the organisational model. Based on this structural information and a description of the organisation’s policies, our approach invalidates the policies and identifies exemplary sequences of actions that lead to a violation of the policy in question. Based on these examples, the organisation can identify real attack vectors that might result in an insider attack. This information can be used to refine access control systems or policies. We provide case studies showing how mechanical verification tools, i.e. modelchecking with MCMAS and interactive theorem proving in Isabelle/HOL, can be applied to support the invalidation and thereby the identification of the attack vectors.
    Original languageEnglish
    Pages (from-to)59-79
    Number of pages6
    JournalJournal of wireless mobile networks, ubiquitous computing, and dependable applications
    Issue number2
    Publication statusPublished - Jun 2014
    EventIEEE Security and Privacy Workshops, SPW 2013 - San Francisco, United States
    Duration: 23 May 201324 May 2013


    • EC Grant Agreement nr.: FP7/318003
    • EC Grant Agreement nr.: FP7/2007-2013
    • Organisational structure
    • Policies
    • Formal methods


    Dive into the research topics of 'Invalidating policies using structural information'. Together they form a unique fingerprint.

    Cite this