Modeling and Verification of Insider Threats Using Logical Analysis

Florian Kammuller, Christian W. Probst

Research output: Contribution to journalJournal articleResearchpeer-review

200 Downloads (Pure)


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
JournalI E E E Systems Journal
Issue number2
Pages (from-to)534-545
Number of pages12
Publication statusPublished - 2017


  • Automated verification
  • Formal modeling
  • Insider threats

Cite this