Verfeinerte Modellierung kryptographischer Protokolle
Was lernen wir aus dem Beispiel?
- Nicht nur E, sondern auch M muß bei jedem kryptographischen Protokoll als Teilnehmer berücksichtigt werden.
- Implizite Annahmen sind zu vermeiden.
D. h., das Protokoll »hybride Verschlüsselung« war unvollständig spezifiziert und dadurch unsicher.
Ziel formaler Spezifikationsmethoden:
- Automatisches Erkennen solcher Unzulänglichkeiten.
Dieses Ziel ist bisher unerreicht &endash; erfolgreicher sind bisher pragmatische Ansätze,
die auf dem »gesunden Menschenverstand« beruhen.
Maßnahmen gegen einen aktiven Angriff
- Vorherige sichere Identifikation der Teilnehmer.
Achtung: Kann M sich in hängende Verbindungen einschalten?
- Erweiterung des Protokolls, hier etwa durch Zertifikate
(weiterer Mitspieler: N).
Achtung: Kooperation von M mit N?
- Zusätzliche Synchronitätsforderungen &endash;
- z. B. künstliches Aufspalten von Nachrichten
(Interlock-Protokoll),
- Zeitstempel,
- parallele Kommunikationskanäle.
- Organisatorische Vorkehrungen &endash;
M das Leben erschweren durch Änderung der Randbedingungen des Protokolls.
Denn M muß bei realer Umsetzung seines Angriffs stets präsent sein, den gesamten
Nachrichtenstrom filtern, also:
- Starke Ressourcen nötig,
- hohes Entdeckungsrisiko.
Verfeinerte Modellierung
Modellierung von M (formal komplizierter als für E).
Evtl. »Vernichten von Daten« modellieren.
Zusätzlich ins Modell einbauen:
»Wissen«: A ist sicher, daß m korrekt ist,
evtl. probabilistisch (»Glauben«).
Modellierung von »Vertrauen«.
...
Noch manches läßt sich modellieren.
Das Problem dabei ist,
- das Modell handhabbar zu halten,
- d. h. so, daß sich noch etwas damit anfangen läßt.
Schwierigkeiten bei Modellierung und Sicherheitsnachweis
- Stimmen die Grundannahmen und Randbedingungen des Protokolls?
- Sind z. B. die kryptographischen Mechanismen sicher?
- Erleichtert das Protokoll die Kryptoanalyse der Grundfunktionen?
- Eröffnet es Möglichkeiten zur Probeverschlüsselung?
- Protokollfallen (z. B. RSA-Falle: versehentliches Entschlüsseln durch [evtl. blinde]
Unterschrift)?
- Stimmt das Verhalten der Teilnehmer?
Welche Möglichkeiten eröffnen Social Engineering, Mogeleien, Kooperationen?
- Welche Folgen haben Einbrüche für den Rest des Protokolls?
Aufdeckung eines Geheimnisses für die übrigen Geheimnisse?
Für künftige Protokollanwendungen?
- Datenabgleich mit äußeren Datenquellen?
Auch mit statistischen Methoden.
- Verdeckte Kanäle?
Formale Analyse kryptographischer Protokolle
A. D. Rubin/ P. Honeyman:
Formal methods for the analysis of authentication protocols.
http://www.citi.umich.edu/techreports/PS.Z/citi-tr-93-7.ps.Z
Klassifikation der Methoden nach Catherine Meadows:
- Allgemeine Spezifikationssprachen und Verifikationsmethoden.
- Expertensysteme, die verschiedenen Szenarien analysieren.
- Logik von Wissen und Glauben formalisieren.
- Algebraische Termersetzungen in kryptographischen Systemen.
Keine Methode führt zu einem vollständigen formalen Sicherheitsbeweis.
Mögliche Attacken müssen spezifiziert werden,
um ihre Unmöglichkeit zu beweisen,
können also nicht automatisch entdeckt werden.
D. h., es ist bestenfalls Sicherheit vor bekannten Angriffen beweisbar.
Alles bisher Bewiesene war auch ohne Formalisierung zu sehen.
Vorlesung Datenschutz und Datensicherheit
Sommersemester 1996, Fachbereich Mathematik
Johannes-Gutenberg-Universität Mainz
Zurück zum Inhaltsverzeichnis
Autor: Klaus Pommerening, 24. Juni 1996; letzte Änderung: 24. September 1996.
E-Mail an Pommerening@imsd.uni-mainz.de.