Combining Generated Data Models with Formal Invalidation for Insider Threat Analysis

Florian Kammuller, Christian W. Probst

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

241 Downloads (Pure)

Abstract

In this paper we revisit the advances made on invalidation policies to explore attack possibilities in organizational models. One aspect that has so far eloped systematic analysis of insider threat is the integration of data into attack scenarios and its exploitation for analyzing the models. We draw from recent insights into generation of insider data to complement a logic based mechanical approach. We show how insider analysis can be traced back to the early days of security verification and the Lowe-attack on NSPK. The invalidation of policies allows modelchecking organizational structures to detect insider attacks. Integration of higher order logic specification techniques allows the use of data refinement to explore attack possibilities beyond the initial system specification. We illustrate this combined invalidation technique on the classical example of the naughty lottery fairy. Data generation techniques support the automatic generation of insider attack data for research. The data generation is however always based on human generated insider attack scenarios that have to be designed based on domain knowledge of counter-intelligence experts. Introducing data refinement and invalidation techniques here allows the systematic exploration of such scenarios and exploit data centric views into insider threat analysis.
Original languageEnglish
Title of host publication2014 IEEE Security and Privacy Workshops (SPW)
PublisherIEEE
Publication date2014
Pages229-235
DOIs
Publication statusPublished - 2014
Event2014 IEEE Security and Privacy Workshops (SPW) - The Fairmont, San Jose, California, United States
Duration: 17 May 201418 May 2014
http://www.ieee-security.org/TC/SPW2014/index.html

Conference

Conference2014 IEEE Security and Privacy Workshops (SPW)
LocationThe Fairmont
CountryUnited States
CitySan Jose, California
Period17/05/201418/05/2014
OtherCo-located with the 35th IEEE Symposium on Security and Privacy (SP)
Internet address

Bibliographical note

WRIT: 2nd Workshop on Research for Insider Threat: http://www.sei.cmu.edu/community/writ2014/writ2014-program.cfm

Keywords

  • Insider threats
  • policies
  • formal methods

Cite this

Kammuller, F., & Probst, C. W. (2014). Combining Generated Data Models with Formal Invalidation for Insider Threat Analysis. In 2014 IEEE Security and Privacy Workshops (SPW) (pp. 229-235). IEEE. https://doi.org/10.1109/SPW.2014.45