{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T12:42:25Z","timestamp":1743079345041,"version":"3.40.3"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319171111"},{"type":"electronic","value":"9783319171128"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17112-8_3","type":"book-chapter","created":{"date-parts":[[2015,6,12]],"date-time":"2015-06-12T11:46:28Z","timestamp":1434109588000},"page":"45-81","source":"Crossref","is-referenced-by-count":1,"title":["Integrating a Model-Driven Approach and Formal Verification for the Development of Secure Service Applications"],"prefix":"10.1007","author":[{"given":"Marian","family":"Borek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kuzman","family":"Katkalov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nina","family":"Moebius","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kurt","family":"Stenzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Alam, M.M., Breu, R., Breu, M.: Model driven security for web services (MDS4WS). In: 8th International Multitopic Conference, 2004. Proceedings of INMIC 2004, pp.\u00a0498\u2013505. IEEE, Piscataway (2004)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, R.J., Needham, R.M.: Programming satan\u2019s computer. In: Computer Science Today, vol. 1000, pp.\u00a0426\u2013440. Springer, Heidelberg (1995)","DOI":"10.1007\/BFb0015258"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., C\u00faellar, J., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Proceedings of TACAS 2012 \u2013 Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 7214. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28756-5_19"},{"key":"3_CR4","unstructured":"Baina, K., Benatallah, B., Casati, F., Toumani, F.: Model-driven web service development. In: Advanced Information Systems Engineering, pp.\u00a0527\u2013543. Springer, Heidelberg (2004)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science, vol. 1783. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-46428-X_25"},{"issue":"3","key":"3_CR6","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D.A. Basin","year":"2005","unstructured":"Basin, D.A., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. 4(3), 181\u2013208 (2005)","journal-title":"Int. J. Inf. Secur."},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1125808.1125810","volume":"15","author":"D. Basin","year":"2006","unstructured":"Basin, D., Doser, J., Lodderstedt, T.: Model driven security: from UML models to access control infrastructures. ACM Trans. Softw. Eng. Methodol. 15, 39\u201391 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Bella, G.: Mechanising a protocol for smart cards. In: Proceedings of e-Smart 2001, International Conference on Research in Smart Cards. Lecture Notes in Computer Science, vol.\u00a02140. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45418-7_3"},{"issue":"1\u20132","key":"3_CR9","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10817-005-9018-6","volume":"36","author":"G. Bella","year":"2006","unstructured":"Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET purchase protocols. J. Automat. Reas. 36(1\u20132), 5\u201337 (2006)","journal-title":"J. Automat. Reas."},{"issue":"4","key":"3_CR10","doi-asserted-by":"crossref","first-page":"363","DOI":"10.3233\/JCS-2009-0339","volume":"17","author":"B. Blanchet","year":"2009","unstructured":"Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur. 17(4), 363\u2013434 (2009)","journal-title":"J. Comput. Secur."},{"key":"3_CR11","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.\u00a062\u201371. IEEE, Piscataway (2012)","DOI":"10.1109\/SEW.2012.13"},{"key":"3_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40561-7_6","volume-title":"Model checking of security-critical applications in a model driven approach","author":"M. Borek","year":"2013","unstructured":"Borek, M., Moebius, N., Stenzel, K., Reif, W.: Model checking of security-critical applications in a model driven approach. In: Software Engineering and Formal Methods. Springer, Heidelberg (2013)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Borek, M., Moebius, N., Stenzel, K., Reif, W.: Security requirements formalized with ocl in a model-driven approach. In: 2013 IEEE Model-Driven Requirements Engineering Workshop (MoDRE). IEEE, Piscataway (2013)","DOI":"10.1109\/MoDRE.2013.6597265"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., S\u00f6rensen, O.: BPMN core modeling concepts: inheritance-based execution semantics. In: Handbook of Conceptual Modeling. Theory, Practice, and Research Challenges, pp.\u00a0287\u2013332. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-15865-0_9"},{"key":"3_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines\u2014A Method for High-Level System Design and Analysis","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"3_CR16","unstructured":"B\u00f6rger, E., Thalheim, B.: Modeling workflows, interaction patterns, web services and business processes: the ASM-based approach. In: Proceedings of ABZ 2008. Lecture Notes in Computer Science, vol. 5238. Springer, Heidelberg (2008)"},{"issue":"1","key":"3_CR17","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18\u201336 (1990)","journal-title":"ACM Trans. Comput. Syst."},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Bushager, A., Zwolinski, M.: Modelling smart card security protocols in systemC TLM. In: IEEE\/IFIP 8th International Conference on Embedded and Ubiquitous Computing, pp.\u00a0637\u2013643. IEEE Computer Society, Piscataway (2010)","DOI":"10.1109\/EUC.2010.102"},{"key":"3_CR19","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.\u00a0115\u2013124. ACM, New York (2004)","DOI":"10.1145\/1035167.1035185"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Dierks, T., Rescorla, E.: The transport layer security (TLS) protocol version 1.2. IETF Network Working Group. http:\/\/www.ietf.org\/rfc\/rfc5246.txt (2008)","DOI":"10.17487\/rfc5246"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proceedings of 22th IEEE Symposium on Foundations of Computer Science. IEEE, Piscataway (1981)","DOI":"10.1109\/SFCS.1981.32"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Foster, H., G\u00f6nczy, L., Koch, N., Mayer, P., Montangero, C., Varr\u00f3, D.: UML extensions for service-oriented systems. In: Rigorous Software Engineering for Service-Oriented Systems, pp.\u00a035\u201360. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-20401-2_4"},{"key":"3_CR23","volume-title":"SEFM 2005 \u2013 3rd IEEE International Conference on Software Engineering and Formal Methods","author":"H. Grandy","year":"2005","unstructured":"Grandy, H., Stenzel, K., Reif, W.: Object-oriented verification kernels for secure Java applications. In: Aichering, B., Beckert, B. (eds.) SEFM 2005 \u2013 3rd IEEE International Conference on Software Engineering and Formal Methods. IEEE, Piscataway (2005)"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Gronmo, R., Skogan, D., Solheim, I., Oldevik, J.: Model-driven web services development. In: 2004 IEEE International Conference on e-Technology, e-Commerce and e-Service, 2004. EEE\u201904, pp.\u00a042\u201345. IEEE, Piscataway (2004)","DOI":"10.1109\/EEE.2004.1287288"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Gr\u00fcnbauer, J., Hollmann, H., J\u00fcrjens, J., Wimmel, G.: Modelling and verification of layered security protocols: a bank application. In: Proceedings of SAFECOMP 2003. Lecture Notes in Computer Science, vol. 2788. Springer, Heidelberg (2003)","DOI":"10.1007\/978-3-540-39878-3_10"},{"key":"3_CR26","unstructured":"Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying smart card applications: an ASM approach. In: International Conference on integrated Formal Methods (iFM) 2007. Lecture Notes in Computer Science, vol.\u00a04591. Springer, Heidelberg (2007)"},{"key":"3_CR27","unstructured":"Huber, F., Molterer, S., Rausch, A., Schatz, B., Sihling, M., Slotosch, O.: Tool supported specification and simulation of distributed systems. In: Proceedings, International Symposium on Software Engineering for Parallel and Distributed Systems, 1998, pp.\u00a0155\u2013164. IEEE, Piscataway (1998)"},{"key":"3_CR28","unstructured":"Java Card 2.2.2 Application Programming Interfaces: http:\/\/www.oracle.com\/technetwork\/java\/\\\\javacard\/specs-138637.html (2006)"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Jensen, J., Jaatun, M.G.: Security in model driven development: a survey. In: Sixth International Conference on Availability, Reliability and Security, ARES 2011. Lecture Notes in Computer Science, pp.\u00a0704\u2013709. Springer, Heidelberg (2011)","DOI":"10.1109\/ARES.2011.110"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Jones, C., Woodcock, J. (eds.): Form. Asp. Comput. 20(1) (2008)","DOI":"10.1007\/s00165-007-0064-1"},{"key":"3_CR31","volume-title":"Developing high-assurance secure systems with UML: a smartcard-based purchase protocol","author":"J. J\u00fcrjens","year":"2004","unstructured":"J\u00fcrjens, J.: Developing high-assurance secure systems with UML: a smartcard-based purchase protocol. In: IEEE International Symposium on High Assurance Systems Engineering. IEEE, Piscataway (2004)"},{"key":"3_CR32","volume-title":"Secure Systems Development with UML","author":"J. J\u00fcrjens","year":"2005","unstructured":"J\u00fcrjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005)"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Kasal, K., Heurix, J., Neubauer, T.: Model-driven development meets security: an evaluation of current approaches. In: 44th Hawaii International Conference on System Sciences (HICSS), pp.\u00a01\u20139. IEEE Computer Society, Piscataway (2011)","DOI":"10.1109\/HICSS.2011.310"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Katkalov, K., Moebius, N., Stenzel, K., Borek, M., Reif, W.: Model-driven testing of security protocols with secureMDD. In: Fifth IFIP International Conference on New Technologies, Mobility and Security (NTMS 2012). IEEE, Piscataway (2012)","DOI":"10.1109\/NTMS.2012.6208678"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Kroiss, C., Koch, N., Knapp, A.: UWE4JSF: a model-driven generation approach for web applications. In: 3rd Workshop on The Web and Requirements Engineering at ICWE 2012. Lecture Notes in Computer Science, vol. 5648, pp.\u00a0493\u2013496. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02818-2_46"},{"issue":"1","key":"3_CR36","first-page":"89","volume":"12","author":"J.C. Lopez Pimental","year":"2008","unstructured":"Lopez Pimental, J.C., Monroy, R.: Formal support to security protocol development: a survey. Computacion y Sistemas 12(1), 89\u2013108 (2008)","journal-title":"Computacion y Sistemas"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 1055, pp.\u00a0147\u2013166. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61042-1_43"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Mayer, P., Schroeder, A., Koch, N.: MDD4SOA: model-driven service orchestration. In: Proceedings of 12th IEEE International EDOC Conference (EDOC 2008). IEEE, Piscataway (2008)","DOI":"10.1109\/EDOC.2008.55"},{"issue":"2","key":"3_CR39","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Program. 26(2), 113\u2013131 (1996)","journal-title":"J. Logic Program."},{"key":"3_CR40","unstructured":"Memon, M., Hafner, M., Breu, R.: SECTISSIMO: a platform-independent framework for security services. In: Proceedings of the First International Modeling Security Workshop. CEUR Workshop Proceedings, vol. 413. http:\/\/ceur-ws.org\/Vol-413\/ (2008)"},{"key":"3_CR41","unstructured":"Mitra, N., Lafon, Y.: SOAP Version 1.2. W3C (2007)"},{"issue":"1","key":"3_CR42","first-page":"59","volume":"1","author":"N. Moebius","year":"2008","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Modeling security-critical applications with UML in the SecureMDD approach. Int. J. Adv. Softw. 1(1), 59\u201379 (2008)","journal-title":"Int. J. Adv. Softw."},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Moebius, N., Stenzel, K., Grandy, H., Reif, W.: Model-driven code generation for secure smart card applications. In: 20th Australian Software Engineering Conference. IEEE, Piscataway (2009)","DOI":"10.1109\/ASWEC.2009.15"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Moebius, N., Stenzel, K., Grandy, H., Reif, W.: SecureMDD: a model-driven development method for secure smart card applications. In: Workshop on Secure Software Engineering, SecSE, at ARES 2009. IEEE, Piscataway (2009)","DOI":"10.1109\/ARES.2009.22"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Formal verification of application-specific security properties in a model-driven approach. In: Proceedings of ESSoS 2010 - International Symposium on Engineering Secure Software and Systems. Lecture Notes in Computer Science, vol. 5965. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-11747-3_13"},{"key":"3_CR46","doi-asserted-by":"publisher","DOI":"10.1145\/2422498.2422507","volume-title":"Incremental development of large, secure smart card applications","author":"N. Moebius","year":"2012","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, New\u00a0York (2012)"},{"key":"3_CR47","unstructured":"Mordani, R., Chinnici, R., Hadley, M.: The Java API for XML-Based Web Services (JAX-WS) 2.0. JCP (2006)"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Murdoch, S.J., Drimer, S., Anderson, R., Bond, M.: Chip and PIN is broken. In: Proceedings of the 2010 IEEE Symposium on Security and Privacy, pp.\u00a0433\u2013446. IEEE, Piscataway (2010)","DOI":"10.1109\/SP.2010.33"},{"key":"3_CR49","unstructured":"Nadalin, A., Kaler, C., Hallam-Baker, P., Monzillo, R.: Web Services Security: SOAP Message Security 1.0. OASIS (2004)"},{"key":"3_CR50","unstructured":"Nadalin, A., Goodner, M., Gudgin, M., Barbir, A., Granqvist, H.: WS-SecurityPolicy 1.2. OASIS (2006)"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Nakamura, Y., Tatsubori, M., Imamura, T., Ono, K.: Model-driven security based on a web services security architecture. In: IEEE International Conference on Services Computing, pp.\u00a07\u201315. IEEE, Piscataway (2005)","DOI":"10.1109\/SCC.2005.66"},{"issue":"12","key":"3_CR52","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"key":"3_CR53","unstructured":"Object Management Group (OMG): Meta Object Facility (MOF) 2.0 Query\/View\/Transformation Specification, Version 1.1. http:\/\/www.omg.org\/spec\/QVT\/1.1\/ (2011)"},{"key":"3_CR54","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6, 85\u2013128 (1998)","journal-title":"J. Comput. Secur."},{"key":"3_CR55","volume-title":"Renegotiating TLS","author":"M. Ray","year":"2009","unstructured":"Ray, M., Dispensa, S.: Renegotiating TLS. Technical Report, PhoneFactor Inc. (2009)"},{"key":"3_CR56","doi-asserted-by":"crossref","unstructured":"Schroeder, A., Mayer, P.: Verifying interaction protocol compliance of service orchestrations. In: Proceedings of the 6th International Conference on Service-Oriented Computing. Lecture Notes in Computer Science, vol. 5364. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-89652-4_44"},{"key":"3_CR57","unstructured":"Sheng, Q.Z., Benatallah, B.: Contextuml: a uml-based modeling language for model-driven development of context-aware web services. In: International Conference on Mobile Business, 2005. ICMB 2005, pp.\u00a0206\u2013212. IEEE, Piscataway (2005)"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"Smith, S., Beaulieu, A., Greg Phillips, W.: Modeling and verifying security protocols using UML 2. In: International Systems Conference (SysCon), pp.\u00a072\u201379. IEEE Computer Society, Piscataway (2011)","DOI":"10.1109\/SYSCON.2011.5929088"},{"key":"3_CR59","doi-asserted-by":"crossref","unstructured":"Stenzel, K., Moebius, N., Reif, W.: Formal verification of QVT transformations for code generation. In: 14th International Conference on Model Driven Engineering Languages and Systems, MODELS 2011. Lecture Notes in Computer Science, vol. 6981. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24485-8_39"},{"issue":"10","key":"3_CR60","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J.: First steps in the verified software grand challenge. IEEE Comput. 39(10), 57\u201364 (2006)","journal-title":"IEEE Comput."},{"key":"3_CR61","unstructured":"Xpand: http:\/\/projects.eclipse.org\/projects\/modeling.m2t.xpand (2009)"}],"container-title":["Texts & Monographs in Symbolic Computation","Correct Software in Web Applications and Web Services"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17112-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T11:22:55Z","timestamp":1676460175000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17112-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319171111","9783319171128"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17112-8_3","relation":{},"ISSN":["0943-853X","2197-8409"],"issn-type":[{"type":"print","value":"0943-853X"},{"type":"electronic","value":"2197-8409"}],"subject":[],"published":{"date-parts":[[2015]]}}}