Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Formal Modelling and Verification of Transactional Web Service Composition: A Refinement and Proof Approach with Event-B Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Integrating a Model-Driven Approach and Formal Verification for the Development of Secure Service Applications

verfasst von : Marian Borek, Kuzman Katkalov, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

Erschienen in: Correct Software in Web Applications and Web Services

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We present SecureMDD, a development method for secure service applications that integrates a model-driven approach with formal specification techniques using abstract state machines (ASMs), refinement to code and verification with the interactive theorem prover KIV. A larger case study is used to highlight various aspects of the method with a focus on services and their formal verification.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Towards a Model of Services Based on Cocreation, Abstraction and Rights Distribution
Nächstes Kapitel A Formal Model of Client-Cloud Interaction
Fußnoten
2
All 21 messages can be found on our web page http://​www.​informatik.​uni-augsburg.​de/​lehrstuehle/​swt/​se/​projects/​secureMDD/​. Some of them are used in the activity diagrams in Figs. 4 and 6.
 
4
implies is an OCL keyword since an arrow -> is used for operations on collections.
 
Literatur
1.
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. 498–505. IEEE, Piscataway (2004)
2.
Anderson, R.J., Needham, R.M.: Programming satan’s computer. In: Computer Science Today, vol. 1000, pp. 426–440. Springer, Heidelberg (1995)
3.
Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cúellar, J., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Proceedings of TACAS 2012 – Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 7214. Springer, Heidelberg (2012)
4.
Baina, K., Benatallah, B., Casati, F., Toumani, F.: Model-driven web service development. In: Advanced Information Systems Engineering, pp. 527–543. Springer, Heidelberg (2004)
5.
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)
6.
Basin, D.A., Mödersheim, S., Viganò, L.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. 4(3), 181–208 (2005)CrossRef
7.
Basin, D., Doser, J., Lodderstedt, T.: Model driven security: from UML models to access control infrastructures. ACM Trans. Softw. Eng. Methodol. 15, 39–91 (2006)CrossRef
8.
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. 2140. Springer, Heidelberg (2001)
9.
Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET purchase protocols. J. Automat. Reas. 36(1–2), 5–37 (2006)MATHCrossRef
10.
Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur. 17(4), 363–434 (2009)
11.
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–71. IEEE, Piscataway (2012)
12.
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)CrossRef
13.
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)
14.
Börger, E., Sörensen, O.: BPMN core modeling concepts: inheritance-based execution semantics. In: Handbook of Conceptual Modeling. Theory, Practice, and Research Challenges, pp. 287–332. Springer, Heidelberg (2011)
15.
Börger, E., Stärk, R.F.: Abstract State Machines—A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)MATHCrossRef
16.
Börger, 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)
17.
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)CrossRef
18.
Bushager, A., Zwolinski, M.: Modelling smart card security protocols in systemC TLM. In: IEEE/IFIP 8th International Conference on Embedded and Ubiquitous Computing, pp. 637–643. IEEE Computer Society, Piscataway (2010)
19.
Deubler, M., Grünbauer, J., Jürjens, J., Wimmel, G.: Sound development of secure service-based systems. In: Proceedings of the 2nd International Conference on Service Oriented Computing, pp. 115–124. ACM, New York (2004)
20.
21.
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)
22.
Foster, H., Gönczy, L., Koch, N., Mayer, P., Montangero, C., Varró, D.: UML extensions for service-oriented systems. In: Rigorous Software Engineering for Service-Oriented Systems, pp. 35–60. Springer, Heidelberg (2011)
23.
Grandy, H., Stenzel, K., Reif, W.: Object-oriented verification kernels for secure Java applications. In: Aichering, B., Beckert, B. (eds.) SEFM 2005 – 3rd IEEE International Conference on Software Engineering and Formal Methods. IEEE, Piscataway (2005)
24.
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’04, pp. 42–45. IEEE, Piscataway (2004)
25.
Grünbauer, J., Hollmann, H., Jürjens, 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)
26.
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. 4591. Springer, Heidelberg (2007)
27.
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. 155–164. IEEE, Piscataway (1998)
28.
29.
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. 704–709. Springer, Heidelberg (2011)
30.
Jones, C., Woodcock, J. (eds.): Form. Asp. Comput. 20(1) (2008)
31.
Jürjens, 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)
32.
Jürjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005)MATH
33.
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. 1–9. IEEE Computer Society, Piscataway (2011)
34.
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)
35.
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. 493–496. Springer, Heidelberg (2009)
36.
Lopez Pimental, J.C., Monroy, R.: Formal support to security protocol development: a survey. Computacion y Sistemas 12(1), 89–108 (2008)
37.
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. 147–166. Springer, Heidelberg (1996)
38.
Mayer, P., Schroeder, A., Koch, N.: MDD4SOA: model-driven service orchestration. In: Proceedings of 12th IEEE International EDOC Conference (EDOC 2008). IEEE, Piscataway (2008)
39.
Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Program. 26(2), 113–131 (1996)MATHCrossRef
40.
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)
41.
Mitra, N., Lafon, Y.: SOAP Version 1.2. W3C (2007)
42.
Moebius, N., Stenzel, K., Reif, W.: Modeling security-critical applications with UML in the SecureMDD approach. Int. J. Adv. Softw. 1(1), 59–79 (2008)
43.
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)
44.
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)
45.
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)
46.
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 York (2012)CrossRef
47.
Mordani, R., Chinnici, R., Hadley, M.: The Java API for XML-Based Web Services (JAX-WS) 2.0. JCP (2006)
48.
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. 433–446. IEEE, Piscataway (2010)
49.
Nadalin, A., Kaler, C., Hallam-Baker, P., Monzillo, R.: Web Services Security: SOAP Message Security 1.0. OASIS (2004)
50.
Nadalin, A., Goodner, M., Gudgin, M., Barbir, A., Granqvist, H.: WS-SecurityPolicy 1.2. OASIS (2006)
51.
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. 7–15. IEEE, Piscataway (2005)
52.
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)MATHCrossRef
53.
54.
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6, 85–128 (1998)
55.
Ray, M., Dispensa, S.: Renegotiating TLS. Technical Report, PhoneFactor Inc. (2009)
56.
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)
57.
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. 206–212. IEEE, Piscataway (2005)
58.
Smith, S., Beaulieu, A., Greg Phillips, W.: Modeling and verifying security protocols using UML 2. In: International Systems Conference (SysCon), pp. 72–79. IEEE Computer Society, Piscataway (2011)
59.
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)
60.
Woodcock, J.: First steps in the verified software grand challenge. IEEE Comput. 39(10), 57–64 (2006)CrossRef
61.
Metadaten
Titel
Integrating a Model-Driven Approach and Formal Verification for the Development of Secure Service Applications
verfasst von
Marian Borek
Kuzman Katkalov
Nina Moebius
Wolfgang Reif
Gerhard Schellhorn
Kurt Stenzel
Copyright-Jahr
2015
Buch
Correct Software in Web Applications and Web Services

Print ISBN: 978-3-319-17111-1

Electronic ISBN: 978-3-319-17112-8

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-17112-8_3