Thorsten Koch promovierte erfolgreich zum Thema „Specification and Verification of Security Protocols and their Utilization in Scenario-based Requirements Engineering“ bei Prof. Dr. Eric Bodden. Dazu gratulieren wir herzlich!
Zusammenfassung der Arbeit:
Security Protokolle spielen eine zentrale Rolle, um die Kommunikation von software-intensiven Systemen vor Cyberangriffen zu schützen. Die korrekte Spezifikation und Anwendung dieser Protokolle ist jedoch langwierig und fehleranfällig.
Mit Hilfe des symbolischen Model-Checkings wird überprüft, ob die Spezifikation korrekt ist und das Protokoll die gewünschten Eigenschaften aufweist. Allerdings reicht ein einzelner Model-Checker nicht aus, um das Protokoll vollständig zu verifizieren. Stattdessen müssen mehrere Model-Checkers verwendet werden. Dies führt zu einer zeitaufwändigen und fehleranfälligen Modellierung desselben Protokolls in verschiedenen Eingabesprachen. Darüber hinaus adressieren die heutigen Ansätze zum Requirements Engineering entweder funktionale oder sicherheits-bezogene Anforderungen. Es ist daher schwer zu beurteilen, ob die spezifizierten Maßnahmen ausreichen, um das System abzusichern, und ob die Maßnahmen zu Konflikten mit anderen funktionalen Anforderungen führen.
Ziel dieser Arbeit ist ein modellbasierter Ansatz zur Spezifikation und Verifikation von Security Protokollen sowie deren Verwendung im szenario-basierten Requirements Engineering. Auf Basis einer UML-konformen Modellierungssprache können Protokolle spezifiziert und automatisch in die Eingabesprache verschiedener Model-Checker überführt werden. Zudem können die spezifizierten Protokolle mit Hilfe eines template-basierten Ansatzes systematisch in eine Anforderungsspezifikation integriert werden.
