{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:58:30Z","timestamp":1770753510360,"version":"3.50.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319170152","type":"print"},{"value":"9783319170169","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17016-9_18","type":"book-chapter","created":{"date-parts":[[2015,3,29]],"date-time":"2015-03-29T00:52:41Z","timestamp":1427590361000},"page":"277-292","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Probabilistic Modelling of Humans in Security Ceremonies"],"prefix":"10.1007","author":[{"given":"Christian","family":"Johansen","sequence":"first","affiliation":[]},{"given":"Audun","family":"J\u00f8sang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,3,28]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, C., Schmidt, D. (eds.) POPL, pp. 104\u2013115. ACM (2001)","DOI":"10.1145\/373243.360213"},{"issue":"1","key":"18_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148(1), 1\u201370 (1999)","journal-title":"Inf. Comput."},{"key":"18_CR3","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-642-30436-1_23","volume-title":"Information Security and Privacy Research","author":"G Bella","year":"2012","unstructured":"Bella, G., Coles-Kemp, L.: Layered analysis of security ceremonies. In: Gritzalis, D., Furnell, S., Theoharidou, M. (eds.) SEC 2012. IFIP AICT, vol. 376, pp. 273\u2013286. Springer, Heidelberg (2012)"},{"issue":"4","key":"18_CR4","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1006\/ijhc.2001.0483","volume":"55","author":"N Bevan","year":"2001","unstructured":"Bevan, N.: International standards for HCI and usability. Int. J. Hum. Comput. Stud. 55(4), 533\u2013552 (2001)","journal-title":"Int. J. Hum. Comput. Stud."},{"key":"18_CR5","volume-title":"Statistical Inference for Markov Processes","author":"P Billingsley","year":"1961","unstructured":"Billingsley, P.: Statistical Inference for Markov Processes. The University of Chicago Press, Chicago (1961)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: IEEE Symposium on Security and Privacy, pp. 86\u2013102. IEEE Computer Society (2004)","DOI":"10.1109\/SECPRI.2004.1301317"},{"issue":"4","key":"18_CR7","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1109\/TDSC.2007.1005","volume":"5","author":"B Blanchet","year":"2008","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Sec. Comput. 5(4), 193\u2013207 (2008)","journal-title":"IEEE Trans. Dependable Sec. Comput."},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Carlos, M.C., Martina, J.E., Price, G., Cust\u00f3dio, R.F.: An updated threat model for security ceremonies. In: Shin, S.Y., Maldonado, J.C. (eds.) 28th Annual ACM Symposium on Applied Computing (SAC 2013), pp. 1836\u20131843. ACM (2013)","DOI":"10.1145\/2480362.2480705"},{"issue":"2","key":"18_CR9","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013207 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"18_CR10","unstructured":"Ellison, C.: Ceremony design and analysis. Cryptology ePrint Archive, Report 2007\/399 (2007)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Ferreira, A., Giustolisi, R., Huynen, J.L., Koenig, V., Lenzini, G.: Studies in socio-technical security analysis: authentication of identities with TLS certificates. In: TrustCom\/ISPA\/IUCC, pp. 1553\u20131558. IEEE (2013)","DOI":"10.1109\/TrustCom.2013.190"},{"issue":"1","key":"18_CR12","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1006\/inco.1995.1123","volume":"121","author":"RJ van Glabbeek","year":"1995","unstructured":"van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121(1), 59\u201380 (1995)","journal-title":"Inf. Comput."},{"key":"18_CR13","volume-title":"Modelling and Analysis of Security Protocols","author":"M Goldsmith","year":"2000","unstructured":"Goldsmith, M., Lowe, G., Roscoe, B., Ryan, P., Schneider, S.: Modelling and Analysis of Security Protocols. Pearson Education, Harlow (2000)"},{"key":"18_CR14","unstructured":"Groote, J.F., Mathijssen, A., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.: The formal specification language mCRL2. In: Methods for Modelling Software Systems (MMOSS 2006). Dagstuhl Seminar Proceedings, vol. 06351 (2007)"},{"key":"18_CR15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-30195-0_16","volume-title":"Grammatical Inference: Algorithms and Applications","author":"C de la Higuera","year":"2004","unstructured":"de la Higuera, C., Oncina, J.: Learning stochastic finite automata. In: Paliouras, G., Sakakibara, Y. (eds.) ICGI 2004. LNCS (LNAI), vol. 3264, pp. 175\u2013186. Springer, Heidelberg (2004)"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1016\/B978-044482830-9\/50029-1","volume-title":"Handbook of Process Algebras","author":"B Jonsson","year":"2001","unstructured":"Jonsson, B., Larsen, K.G., Yi, W.: Probabilistic extensions of process algebras. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebras, pp. 685\u2013711. Elsevier, Amsterdam (2001)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Advances and challenges of probabilistic model checking. In: Proceedings of the 48th Annual Allerton Conference on Communication, Control and Computing, pp. 1691\u20131698. IEEE Press (2010)","DOI":"10.1109\/ALLERTON.2010.5707120"},{"issue":"1","key":"18_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"18_CR20","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780199256044.001.0001","volume-title":"Reassembling the Social - An Introduction to Actor-Network-Theory","author":"B Latour","year":"2005","unstructured":"Latour, B.: Reassembling the Social - An Introduction to Actor-Network-Theory. Oxford University Press, Oxford (2005)"},{"issue":"3","key":"18_CR21","first-page":"93","volume":"17","author":"G Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the needham-schroeder public-key protocol using FDR. Softw. Concepts Tools 17(3), 93\u2013102 (1996)","journal-title":"Softw. Concepts Tools"},{"key":"18_CR22","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: IEEE Symposium on Security and Privacy, pp. 141\u2013151. IEEE Computer Society (1997)"},{"key":"18_CR23","volume-title":"Unified Theories of Cognition","author":"A Newell","year":"1990","unstructured":"Newell, A.: Unified Theories of Cognition. Harvard University Press, Cambridge (1990)"},{"issue":"2","key":"18_CR24","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","volume":"43","author":"G Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Meth. Syst. Des. 43(2), 164\u2013190 (2013)","journal-title":"Formal Meth. Syst. Des."},{"issue":"1\u20132","key":"18_CR25","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"LC Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1\u20132), 85\u2013128 (1998)","journal-title":"J. Comput. Secur."},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Pavlovic, D., Meadows, C.: Actor-network procedures: modeling multi-factor authentication, device pairing, social interactions. arXiv.org (2011)","DOI":"10.1007\/978-3-642-28073-3_2"},{"issue":"1","key":"18_CR27","first-page":"75","volume":"2","author":"W Pieters","year":"2011","unstructured":"Pieters, W.: Representing humans in system security models: an actor-network approach. J. Wirel. Mob. Netw. Ubiquit. Comput. Dependable Appl. 2(1), 75\u201392 (2011)","journal-title":"J. Wirel. Mob. Netw. Ubiquit. Comput. Dependable Appl."},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Process logic. In: 6th Symposium on Principles of Programming Languages (POPL 1979), pp. 93\u2013100. ACM (1979)","DOI":"10.1145\/567752.567761"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Prisacariu, C.: Actor network procedures as psi-calculi for security ceremonies. In: International Workshop on Graphical Models for Security. Electronic Proceedings in Theoretical Computer Science, vol. 148, pp. 63\u201377. Open Publishing Assoc. (2014)","DOI":"10.4204\/EPTCS.148.5"},{"issue":"3","key":"18_CR30","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/S0019-9958(63)90290-0","volume":"6","author":"MO Rabin","year":"1963","unstructured":"Rabin, M.O.: Probabilistic automata. Inform. Control 6(3), 230\u2013245 (1963)","journal-title":"Inform. Control"},{"key":"18_CR31","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-21424-0_9","volume-title":"Future Challenges in Security and Privacy for Academia and Industry","author":"K Radke","year":"2011","unstructured":"Radke, K., Boyd, C., Gonzalez Nieto, J., Brereton, M.: Ceremony analysis: strengths and weaknesses. In: Camenisch, J., Fischer-H\u00fcbner, S., Murayama, Y., Portmann, A., Rieder, C. (eds.) SEC 2011. IFIP AICT, vol. 354, pp. 104\u2013115. Springer, Heidelberg (2011)"},{"key":"18_CR32","volume-title":"Interaction Design: Beyond Human-Computer Interaction","author":"Y Rogers","year":"2011","unstructured":"Rogers, Y., Sharp, H., Preece, J.: Interaction Design: Beyond Human-Computer Interaction, 3rd edn. Wiley, Chichester (2011)","edition":"3"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-540-69554-7_10","volume-title":"Interactive Systems","author":"R Ruk\u0161\u0117nas","year":"2007","unstructured":"Ruk\u0161\u0117nas, R., Curzon, P., Back, J., Blandford, A.: Formal modelling of cognitive interpretation. In: Doherty, G., Blandford, A. (eds.) DSVIS 2006. LNCS, vol. 4323, pp. 123\u2013136. Springer, Heidelberg (2007)"},{"issue":"2","key":"18_CR34","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s11334-008-0050-7","volume":"4","author":"R Ruksenas","year":"2008","unstructured":"Ruksenas, R., Curzon, P., Blandford, A.: Modelling and analysing cognitive causes of security breaches. Innovations Sys. Softw. Eng. 4(2), 143\u2013160 (2008)","journal-title":"Innovations Sys. Softw. Eng."},{"issue":"3\/4","key":"18_CR35","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF01028968","volume":"51","author":"K Segerberg","year":"1992","unstructured":"Segerberg, K.: Getting started: beginnings in the logic of action. Stud. Logica 51(3\/4), 347\u2013378 (1992)","journal-title":"Stud. Logica"},{"issue":"2","key":"18_CR36","first-page":"105","volume":"26","author":"R Seman\u010d\u00edk","year":"2007","unstructured":"Seman\u010d\u00edk, R.: Basic properties of the persona model. Comput. Inform. 26(2), 105\u2013121 (2007)","journal-title":"Comput. Inform."},{"key":"18_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24611-4_1","volume-title":"Validation of Stochastic Systems","author":"A Sokolova","year":"2004","unstructured":"Sokolova, A., de Vink, E.P.: Probabilistic automata: system types, parallel composition and comparison. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 1\u201343. Springer, Heidelberg (2004)"},{"key":"18_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Computer Aided Verification","author":"U Stern","year":"1997","unstructured":"Stern, U., Dill, D.L.: Parallelizing the Mur$$\\varphi $$ verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256\u2013278. Springer, Heidelberg (1997)"},{"key":"18_CR39","unstructured":"Teodorescu, I.: Maximum likelihood estimation for markov chains (2009). arxiv:0905.4131"}],"container-title":["Lecture Notes in Computer Science","Data Privacy Management, Autonomous Spontaneous Security, and Security Assurance"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17016-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T18:12:54Z","timestamp":1747851174000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17016-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319170152","9783319170169"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17016-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"28 March 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}