Modeling and verification of insider threats using logical analysis

Florian Kammüller, Christian W. Probst

    Research output: Contribution to journalArticleAcademicpeer-review

    13 Citations (Scopus)


    In this paper, we combine formal modeling and analysis of infrastructures of organizations with sociological explanation to provide a framework for insider threat analysis. We use the higher order logic (HOL) proof assistant Isabelle/HOL to support this framework. In the formal model, we exhibit and use a common trick from the formal verification of security protocols, showing that it is applicable to insider threats. We introduce briefly a three-step process of social explanation, illustrating that it can be applied fruitfully to the characterization of insider threats. We introduce the insider theory constructed in Isabelle that implements this process of social explanation. To validate that the social explanation is generally useful for the analysis of insider threats and to demonstrate our framework, we model and verify the insider threat patterns of entitled independent and Ambitious Leader in our Isabelle/HOL framework.
    Original languageEnglish
    Pages (from-to)534-545
    Number of pages12
    JournalIEEE systems journal
    Issue number2
    Publication statusPublished - 2016


    • EC Grant Agreement nr.: FP7/318003
    • SCS-Cybersecurity
    • Formal modeling
    • EC Grant Agreement nr.: FP7/2007-2013
    • Automated verification
    • Insider threats


    Dive into the research topics of 'Modeling and verification of insider threats using logical analysis'. Together they form a unique fingerprint.

    Cite this