{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:59:57Z","timestamp":1748350797536},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642405600"},{"type":"electronic","value":"9783642405617"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40561-7_6","type":"book-chapter","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T13:10:29Z","timestamp":1379509829000},"page":"76-90","source":"Crossref","is-referenced-by-count":8,"title":["Model Checking of Security-Critical Applications in a Model-Driven Approach"],"prefix":"10.1007","author":[{"given":"Marian","family":"Borek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nina","family":"Moebius","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kurt","family":"Stenzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-28756-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Armando","year":"2012","unstructured":"Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 267\u2013282. Springer, Heidelberg (2012)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L., Cuellar, J., Tobarra, L.: Formal analysis of saml 2.0 web browser single sign-on: breaking the saml-based single sign-on for google apps. In: Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering, pp. 1\u201310. ACM (2008)","DOI":"10.1145\/1456396.1456397"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-642-19125-1_3","volume-title":"Engineering Secure Software and Systems","author":"W. Arsac","year":"2011","unstructured":"Arsac, W., Compagna, L., Pellegrino, G., Ponta, S.E.: Security validation of business processes via model-checking. In: Erlingsson, \u00da., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol.\u00a06542, pp. 29\u201342. Springer, Heidelberg (2011)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Balser","year":"2000","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 363\u2013366. Springer, Heidelberg (2000)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Basin, D., Doser, J., Lodderstedt, T.: Model Driven Security: From UML Models to Access Control Infrastructures. ACM Transactions on Software Engineering and Methodology, 39\u201391 (2006)","DOI":"10.1145\/1125808.1125810"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Borek, M., Moebius, N., Stenzel, K., Reif, W.: Model-driven development of secure service applications. In: 2012 35th Annual IEEE Software Engineering Workshop (SEW), pp. 62\u201371. IEEE (2012)","DOI":"10.1109\/SEW.2012.13"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Deubler, M., Gr\u00fcnbauer, J., J\u00fcrjens, J., Wimmel, G.: Sound development of secure service-based systems. In: Proceedings of the 2nd International Conference on Service Oriented Computing, pp. 115\u2013124. ACM (2004)","DOI":"10.1145\/1035167.1035185"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.C.: On the Security of Public Key Protocols. In: Proc. 22nd IEEE Symposium on Foundations of Computer Science. IEEE (1981)","DOI":"10.1109\/SFCS.1981.32"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"issue":"5","key":"6_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker spin. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"6_CR13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/JCS-2001-91-202","volume":"9","author":"M.L. Hui","year":"2001","unstructured":"Hui, M.L., Lowe, G.: Fault-preserving simplifying transformations for security protocols. Journal of Computer Security\u00a09(1), 3\u201346 (2001)","journal-title":"Journal of Computer Security"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/11554578_2","volume-title":"Foundations of Security Analysis and Design III","author":"J. J\u00fcrjens","year":"2005","unstructured":"J\u00fcrjens, J.: Model-based security engineering with UML. In: Aldini, A., Gorrieri, R., Martinelli, F. (eds.) FOSAD 2004\/2005. LNCS, vol.\u00a03655, pp. 42\u201377. Springer, Heidelberg (2005)"},{"key":"6_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-03829-7_6","volume-title":"Foundations of Security Analysis and Design V","author":"S. M\u00f6dersheim","year":"2009","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L.: The open-source fixed-point model checker for symbolic analysis of security protocols. In: Foundations of Security Analysis and Design V. LNCS, vol.\u00a05705, pp. 166\u2013194. Springer, Heidelberg (2009)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Moebius, N., Stenzel, K., Borek, M., Reif, W.: Incremental development of large, secure smart card applications. In: Proceedings of the Workshop on Model-Driven Security. ACM (2012)","DOI":"10.1145\/2422498.2422507"},{"key":"6_CR17","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Modeling Security-Critical Applications with UML in the SecureMDD Approach. International Journal on Advances in Software\u00a01(1) (2008)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-11747-3_13","volume-title":"Engineering Secure Software and Systems","author":"N. Moebius","year":"2010","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Formal verification of application-specific security properties in a model-driven approach. In: Massacci, F., Wallach, D., Zannone, N. (eds.) ESSoS 2010. LNCS, vol.\u00a05965, pp. 166\u2013181. Springer, Heidelberg (2010)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/11805618_21","volume-title":"Term Rewriting and Applications","author":"M. Turuani","year":"2006","unstructured":"Turuani, M.: The CL-atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 277\u2013286. Springer, Heidelberg (2006)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-25271-6_1","volume-title":"Formal Methods for Components and Objects","author":"D. Oheimb von","year":"2011","unstructured":"von Oheimb, D., M\u00f6dersheim, S.: ASLan++ \u2014 A formal security specification language for distributed systems. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 1\u201322. Springer, Heidelberg (2011)"},{"key":"6_CR21","unstructured":"ZDNet. Attackers hit google single sign-on password system (2010)"},{"key":"6_CR22","unstructured":"ZDNet. Chip and pin is broken, say researchers (2010)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40561-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T11:19:24Z","timestamp":1558091964000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40561-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405600","9783642405617"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40561-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}