Der weitverbreitete Einsatz von software-intensiven Systemen erhöht das Risiko von Cyberangriffen. Um dieses Risiko zu reduzieren, müssen daher verschiedene absichernde Maßnahmen wie Sicherheitsprotokolle in die Systeme integriert werden. Die korrekte Spezifikation und Anwendung dieser Protokolle ist jedoch mühsam und fehleranfällig. Bei der Spezifikation verwenden Sicherheitsexperten verschiedene symbolische Model-Checker. Allerdings reicht ein einzelner symbolischer Model-Checker nicht aus, um die Sicherheit vollständig zu verifizieren. Daher benötigen Sicherheitsexperten Hilfe bei der Übersetzung eines Sicherheitsprotokolls in die Eingabesprache verschiedener symbolischer Model-Checker, um die zeitaufwändige und fehleranfällige Modellierung desselben Sicherheitsprotokolls zu vermeiden. Darüber hinaus adressieren die heutigen Ansätze zum Requirements Engineering entweder funktionale oder sicherheits-bezogene Anforderungen. Anforderungsmanagern fällt es daher schwer zu beurteilen, ob die spezifizierten Maßnahmen ausreichen das System abzusichern oder ob sie zu Konflikten mit anderen funktionalen Anforderungen führen. In dieser Arbeit wird ein modellbasierter Ansatz zur Spezifikation und Verifikation von Sicherheitsprotokollen sowie deren Verwendung im szenario-basierten Requirements Engineering vorgestellt. Auf Basis einer UML-konformen Modellierungssprache können Sicherheitsprotokolle spezifiziert und automatisch in die Eingabesprache verschiedener symbolischer Model-Checker überführt werden. Zudem können die spezifizierten Protokolle systematisch in eine Anforderungsspezifikation integriert werden. Die Evaluierung anhand von Fallstudien auf Basis realistischer Beispiele zeigt, dass die Beiträge dieser Arbeit in der Praxis anwendbar sind.

The widespread usage of software-intensive systems significantly increases the risk of cyber-attacks. Software-intensive systems must integrate security measures like security protocols to cope with this risk. The correct specification and application of security protocols are tedious and error-prone. When specifying security protocols, security engineers use symbolic model checking to verify the security of the protocols. However, using more than one symbolic model checker is recommended for a thorough and confident analysis. Thus, security engineers need help transforming a security protocol into the input language of different symbolic model checkers to avoid the time-consuming and error-prone remodeling of the same security protocol. In addition, current requirements-engineering approaches address either functional or security-related requirements. Hence, requirements engineers need help to assess whether the applied security measures are sufficient to secure the system and whether the measures lead to conflicts with other functional requirements. To cope with these challenges, we propose a systematic model-based approach for specifying and verifying security protocols in the symbolic model and utilizing them in a scenario-based requirements engineering methodology. Based on a UML-compliant modeling language, security engineers can specify security protocols and automatically analyze them using various symbolic model checkers. In addition, requirements engineers can systematically integrate the verified security protocols into requirements specifications. Furthermore, they can specify misuse cases against the system under development and validate whether it is sufficiently secure to mitigate them. We conduct case studies for all our contributions based on realistic examples and show that our contributions are applicable in practice.