{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T12:16:11Z","timestamp":1744287371241},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319470719"},{"type":"electronic","value":"9783319470726"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47072-6_13","type":"book-chapter","created":{"date-parts":[[2016,9,20]],"date-time":"2016-09-20T21:20:20Z","timestamp":1474406420000},"page":"196-210","source":"Crossref","is-referenced-by-count":4,"title":["Isabelle Modelchecking for Insider Threats"],"prefix":"10.1007","author":[{"given":"Florian","family":"Kamm\u00fcller","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"13_CR1","unstructured":"Kamm\u00fcller, F.: Isabelle insider framework including modelchecking and examples (2016). https:\/\/www.dropbox.com\/sh\/rx8d09pf31cv8bd\/AAALKtaP8HMX642fi04Og4NLa?dl=0"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Axelrad, E.T., Sticha, P.J., Brdiczka, O., Shen, J.: A Bayesian network model for predicting insider threats. In: IEEE Security and Privacy Workshops, SPW-WRIT (2013)","DOI":"10.1109\/SPW.2013.35"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Bishop, M., Conboy, H.M., Phan, H., Simidchieva, B.I., Avrunin, G.S., Clarke, L.A., Osterweil, L.J., Peisert, S.: Insider threat identification by process analysis. In: IEEE Security and Privacy Workshops, SPW-WRIT (2014)","DOI":"10.1109\/SPW.2014.40"},{"key":"13_CR4","unstructured":"Bitdefender. Bitdefender research exposes security risks of android wearable devices (2014). http:\/\/www.darkreading.com\/partner-perspectives\/bitdefender\/bitdefender-research-exposes-security-risks-of-android-wearable-devices-\/a\/d-id\/1318005"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Boender, J., Ivanova, M.G., Kamm\u00fcller, F., Primiero, G.: Modeling human behaviour with higher order logic: insider threats. In: STAST 2014, Co-located with CSF 2014 in the Vienna Summer of Logic. IEEE (2014)","DOI":"10.1109\/STAST.2014.13"},{"key":"13_CR6","volume-title":"Guide to Insider Threats: How to Prevent, Detect, and Respond to Information Technology Crimes (Theft, Sabotage, Fraud)","author":"DM Cappelli","year":"2012","unstructured":"Cappelli, D.M., Moore, A.P., Trzeciak, R.F., The, C.: Guide to Insider Threats: How to Prevent, Detect, and Respond to Information Technology Crimes (Theft, Sabotage, Fraud). Addison-Wesley, Boston (2012)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","first-page":"178","volume-title":"Human Aspects of Information Security, Privacy, and Trust","author":"T Chen","year":"2015","unstructured":"Chen, T., Kamm\u00fcller, F., Nemli, I., Probst, C.W.: A probabilistic analysis framework for malicious insider threats. In: Tryfonas, T., Askoxylakis, I. (eds.) HAS 2015. LNCS, vol. 9190, pp. 178\u2013189. Springer, Heidelberg (2015)"},{"key":"13_CR8","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463\u2013478. Springer, Heidelberg (2013)"},{"key":"13_CR10","volume-title":"Soziologie - Allgemeine Grundlagen","author":"H Esser","year":"1993","unstructured":"Esser, H.: Soziologie - Allgemeine Grundlagen. Campus, Frankfurt (1993)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Greitzer, F.L., Strozer, J.R., Cohen, S., Moore, A.P., Mundie, D., Cowley, J.: Analysis of unintentional insider threats deriving from social engineering exploits. In: IEEE Security and Privacy Workshops, SPW-WRIT (2014)","DOI":"10.1109\/SPW.2014.39"},{"key":"13_CR12","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1086\/286983","volume":"15","author":"CG Hempel","year":"1948","unstructured":"Hempel, C.G., Oppenheim, P.: Studies in the logic of explanation. Philos. Sci. 15, 135\u2013175 (1948)","journal-title":"Philos. Sci."},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/978-3-642-04167-9_9","volume-title":"Formal Methods for Components and Objects","author":"L Henrio","year":"2009","unstructured":"Henrio, L., Kamm\u00fcller, F., Rivera, M.: An asynchronous distributed component model and its semantics. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 159\u2013179. Springer, Heidelberg (2009)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/978-3-319-29968-6_6","volume-title":"Graphical Models for Security","author":"MG Ivanova","year":"2016","unstructured":"Ivanova, M.G., Probst, C.W., Hansen, R.R., Kamm\u00fcller, F.: Transforming graphical system models to graphical attack models. In: Mauw, S., Kordy, B., Jajodia, S. (eds.) GraMSec 2015. LNCS, vol. 9390, pp. 82\u201396. Springer, Heidelberg (2016)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F., Kerber, M.: Investigating airplane safety and security against insider threats using logical modeling. In: IEEE Security and Privacy Workshops, SPW-WRIT. IEEE (2016)","DOI":"10.1109\/SPW.2016.47"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/978-3-319-39381-0_21","volume-title":"Human Aspects of Information Security, Privacy, and Trust","author":"F Kamm\u00fcller","year":"2016","unstructured":"Kamm\u00fcller, F., Nurse, J.R.C., Probst, C.W.: Attack tree analysis for insider threats on the IoT using isabelle. In: Tryfonas, T. (ed.) HAS 2016. LNCS, vol. 9750, pp. 234\u2013246. Springer, Heidelberg (2016)"},{"issue":"3","key":"13_CR17","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1023\/A:1006269330992","volume":"23","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Paulson, L.C.: A formal proof of Sylow\u2019s theorem. J. Autom. Reasoning 23(3), 235\u2013264 (1999)","journal-title":"J. Autom. Reasoning"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F., Probst, C.W.: Invalidating policies using structural information. In: IEEE Security and Privacy Workshops, SPW-WRIT (2013)","DOI":"10.1109\/SPW.2013.36"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F., Probst, C.W.: Combining generated data models with formal invalidation for insider threat analysis. In: IEEE Security and Privacy Workshops, SPW-WRIT (2014)","DOI":"10.1109\/SPW.2014.45"},{"issue":"99","key":"13_CR20","first-page":"1","volume":"PP","author":"F Kamm\u00fcller","year":"2016","unstructured":"Kamm\u00fcller, F., Probst, C.W.: Modeling and verification of insider threats using logical analysis. IEEE Syst. J. PP(99), 1\u201312 (2016). Digital Espionage, and Counter Intelligence. Special issue on Insider Threats to Information Security","journal-title":"IEEE Syst. J."},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales - a sectioning concept for isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149\u2013165. Springer, Heidelberg (1999)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Nurse, J.R.C., Buckley, O., Legg, P.A., Goldsmith, M., Creese, S., Wright, G.R.T., Whitty, M.: Understanding insider threat: a framework for characterising attacks. In: IEEE Security and Privacy Workshops, SPW-WRIT (2014)","DOI":"10.1109\/SPW.2014.38"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Nurse, J.R.C., Erola, A., Agrafiotis, I., Goldsmith, M., Creese, S.: Smart insiders: exploring the threat from insiders using the internet-of-things. In: International Workshop on Secure Internet of Things (SIoT ), in conjunction with ESORICS 2015, LNCS. Springer (2015, in print)","DOI":"10.1109\/SIOT.2015.10"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-319-27810-0_3","volume-title":"Semantics, Logics, and Calculi","author":"CW Probst","year":"2016","unstructured":"Probst, C.W., Kamm\u00fcller, F., Hansen, R.R.: Formal modelling and analysis of\u00a0socio-technical systems. In: Probst, C.W., Hankin, C., Hansen, R.R. (eds.) Semantics, Logics, and Calculi. LNCS, vol. 9560, pp. 54\u201373. Springer, Heidelberg (2016)"},{"key":"13_CR25","unstructured":"Symantec. How safe is your quantified self? Tech. Rep. (2014)"},{"key":"13_CR26","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretic fixpoint theorem and its applications. Pac. J. Math. 5, 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"key":"13_CR27","unstructured":"VERIS. Veris: the vocabulary for event recording and incident sharing (2015). http:\/\/veriscommunity.net"}],"container-title":["Lecture Notes in Computer Science","Data Privacy Management and Security Assurance"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47072-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T19:17:10Z","timestamp":1498331830000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47072-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319470719","9783319470726"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47072-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}