Bachelorarbeit

Einsatz von Model Checking für IT-sicherheitskritische Systeme auf Basis von Angreifermodellen

Zusammenfassung

Model Checking ist ein formales Verfahren zur vollautomatischen Verifikation bzw. Widerlegung der Gültigkeit vorgegebener Eigenschaften in einem Verhaltensmodell. In der IT-Sicherheit kann dieses Verfahren Einsatz finden, um das Vorliegen bestimmter IT-Sicherheitseigenschaften, etwa in Bezug auf Informationsvertraulichkeit und Datenintegrität bei Sicherheitsprotokollen nachzuweisen. Hierzu bietet es sich an, das Systemmodell um sog. Angreifermodelle (z.B. nach Dolev-Yao) zu erweitern, die unterschiedliche Fähigkeiten und Wissensstände eines Angreifers zu erfassen erlauben. Im Rahmen dieser Arbeit sind zunächst bestehende Angreifermodelle und Formalismen zur Beschreibung o.g. Sicherheitsziele zu ermitteln. Darauf aufbauend ist anschließend eine Auswahl an bestehenden Sicherheitsprotokollen hinsichtlich der Erfüllung vorgegebener Sicherheitsziele zu untersuchen. Hierzu ist ein Framework zu entwickeln, welches es dem Benutzer erlaubt, durch Zustandstransitionssysteme modellierte Sicherheitsprotokolle um IT-sicherheitsspezifische atomare Aussagen und ausgewählte Angreifermodelle zu erweitern und diese anschließend einer Verifikation durch Model Checking zu unterziehen.

Bearbeiter: Daniel Dehmel

Betreuer: Dipl.-Inf. David Föhrweiser