The subject of this thesis is the systematic development of secure systems. Security is a complex non-functional requirement affecting all parts of a system at all levels of detail and depending crucially on the assumptions about the system environment. Almost daily, new vulnerabilities are found, often exposing the concerned systems to attacks that result in severe damage.

In this thesis, we describe approaches for the integrated application of model-based development techniques with the aim to improve the security of the developed systems. Of central importance is the integration of security-related aspects into design models and the definition of security-specific development activities based on the extended models. For this purpose, we use a specification language with a formally defined semantics, to eliminate the potential of flaws because of ambiguities in the specifications. An important feature of our work is the provision of tool support, to reduce the necessary effort and experience required from the developer.

As part of our methodology, we present an approach to automatically generate a threat scenario from a model based on the included security-related information, and show how to use threat scenarios to formally verify security requirements by model checking.

Testing is necessary to gain confidence in the security of an implementation, but is not sufficiently integrated into current specification and verification methods for security-critical systems. We describe an approach for security testing based on the extended models. The described approach addresses both the problem of the generation of test sequences likely to discover potential vulnerabilities and the problem of the concretisation of the abstract representations of messages and in particular of cryptography that are employed in current approaches for the specification and verification of security-critical systems to make verification feasible.

We also address top-down oriented development of security-critical systems, where security aspects are first specified in the form of abstract assumptions, which are later realised by applying appropriate security mechanisms. In particular, we elaborate on security mechanisms whose insertion preserves the validity of the security requirements fulfilled with respect to the abstract assumptions. We apply these concepts to the modular specification and analysis of layered security protocols.

The practical applicability of the presented approaches is demonstrated in several case studies from the domain of electronic business and cryptographic protocols.

Gegenstand dieser Arbeit ist die systematische Entwicklung sicherer Systeme. Sicherheit ist eine komplexe nichtfunktionale Anforderung, die stets alle Teile eines Systems auf allen Detaillierungsstufen betrifft und entscheidend von den über die Systemumgebung getroffenen Annahmen abhängt. Fast täglich werden neue Schwachstellen gefunden, die die betroffenen Systeme oft Angriffen aussetzen, die schwere Schäden verursachen.

Die Arbeit beschreibt Ansätze für die integrierte Anwendung modellbasierter Entwicklungsmethoden mit dem Ziel, die Sicherheit der entwickelten Systeme zu verbessern. Von zentraler Bedeutung ist die Integration sicherheitsbezogener Aspekte in Designmodelle und die Definition sicherheitsspezifischer Entwicklungsaktivitäten basierend auf den erweiterten Modellen. Zu diesem Zweck wird eine Spezifikationssprache mit einer formal definierten Semantik genutzt, um Fehler aufgrund von Mehrdeutigkeiten in der Spezifikation zu vermeiden. Um den für die sicherheitsspezifischen Aktivitäten nötigen Aufwand und das erforderliche Expertenwissen möglichst gering zu halten, wird im Rahmen der Arbeit eine geeignete Werkzeugunterstützung zur Verfügung gestellt.

Als Teil der beschriebenen Entwicklungsmethodik wird ein Ansatz zur automatischen Generierung eines Bedrohungsszenarios aus einem Modell unter Ausnutzung der sicherheitsbezogenen Informationen dargestellt. Bedrohungsszenarien bilden die Basis für die formale Verifikation von Sicherheitsanforderungen mit Hilfe von Model Checking.

Testen ist notwendig, um Vertrauen in die Sicherheit einer Implementierung zu gewinnen, ist jedoch bisher ungenügend in Spezifikations- und Verifikationsmethoden für sicherheitskritische Systeme integriert. In der Arbeit wird ein Ansatz für modellbasiertes Sicherheitstesten vorgestellt. Hierbei wird sowohl die Generierung von Testsequenzen behandelt mit dem Ziel, Schwachstellen in der Implementierung zu finden, als auch die Konkretisierung der verwendeten abstrakten Repräsentationen von Nachrichten und insbesondere von kryptographischen Operationen.

Die beschriebene Entwicklungsmethodik unterstützt die Top-Down orientierte Entwicklung sicherheitskritischer Systeme, indem Sicherheitsaspekte zunächst in Form abstrakter Annahmen spezifiziert und in einem späteren Schritt durch geeignete Mechanismen realisiert werden können. Insbesondere werden Sicherheitsmechanismen betrachtet, bei deren Anwendung die Gültigkeit von Sicherheitsanforderungen erhalten bleibt. Die entwickelten Konzepte werden auf die modulare Spezifikation und Analyse geschichteter Sicherheitsprotokolle angewendet.

Die praktische Anwendbarkeit der vorgestellten Ansätze wird anhand einer Reihe von Fallstudien aus den Bereichen E-Business und kryptographische Protokolle demonstriert.