Lehr- und Forschungseinheit für Theoretische Informatik,
Institut für Informatik
der Ludwig-Maximilians-Universität München
2-stündige Vorlesung im Hauptstudium (SS 2005):
- Vorlesung:
- Dr. David von Oheimb, Siemens Corporate Technology, Abteilung für Informationssicherheit
- Zeit: Mittwochs 8:30 - 10:00
- Ort: Raum Oe 1.13, Oettingenstraße 67
- Beginn: 13. April 2005
- Übung:
- keine
- Vorkenntnisse:
-
Grundkenntnisse im Bereich Formale Methoden/Logik
Vorkenntnisse im Bereich Informationssicherheit sind nicht erforderlich.
- Hörerkreis:
- Studierende der Informatik oder Mathematik im Hauptstudium,
- die Theorie und Praxis verbinden möchten.
- Schein:
- Scheinerwerb möglich durch mündliche Prüfung
Unter IT-Sicherheit verstehen wir den Schutz
z.B. der Vertraulichkeit und Integrität bestimmter Daten
gegen mutwillige Angriffe.
Sicherheit ist Voraussetzung für den Betrieb und die Akzeptanz moderner
IT-Systeme, aber aufgrund ihrer Komplexität nur schwer nachzuweisen.
Die verlässlichste Methode, die sicherheitsrelevanten Funktionen und
Sicherheitsziele eines Systems
zu überprüfen und mögliche Schwachstellen aufzudecken, ist
eine formale, also mathematisch-exakte Analyse.
In dieser Spezialvorlesung werden - nach einer allgemeinen Einführung in
das Thema IT-Sicherheit und formale Methoden - industriell relevante Techniken
zur formalen Spezifikation und Analyse von IT-Sicherheit vorgestellt, bewertet,
und ihre praktische Anwendung vorgestellt:
- Automatenmodelle zur Beschreibung reaktiver Systeme
- Verschiedene Zugriffskontrollmodelle, z.B. rollenbasierte und
das klassische Bell-LaPadula-Sicherheitsmodell
- Analyse von Informationsflüssen z.B. durch Noninterference
- Modellierung und Analyse von Kryptoprotokollen mit Modelcheckern
- Aktuelle Beispiele aus der Zertifizierung von Infineon SmardCard-Chips
nach ITSEC und den Common Criteria
- Einführung in IT-Sicherheit und formale Modellierung
- Zugriffskontrolle
Beispiel: Infineon SLE88 MMU
- Evaluierung und Zertifizierung
Beispiel: Infineon SLE66
- Bell-LaPadula-Modell und Varianten
- Informationsfluss
Beispiel: Infineon SLE66
- Kryptoprotokoll-Analyse
Beispiel: Needham-Schroeder Public-Key Protocol
- Vorlesungsfolien, die jeweils kurz nach
den Vorlesungsstunden hier inkrementell zur Verfügung gestellt werden.
- Aktuelle Artikel und Forschungsarbeiten, die in der Vorlesung
bekannt gegeben werden. Insbesondere:
- Einführende Bücher werden ebenfalls in der Vorlesung bekannt gegeben, insbesondere:
- Interacting State Machines
- Zustandsautomatien zur Modellierung von verteilten reaktiven Systemen
- EU-Projekt AVISPA
- Automatische Validierung von Internet-Security-Protokollen und Anwendungen