Was lernen wir aus dem Beispiel?

Wir wollten die Vertraulichkeit schützen und nahmen daher an, dass E die Angreiferin ist. Aber:

• Nicht nur E, sondern auch M muss bei jedem kryptographischen Protokoll als Teilnehmer berücksichtigt werden - auch wenn es »nur« um die Vertraulichkeit geht.
• 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 - erfolgreicher sind pragmatische Ansätze, die auf dem »gesunden Menschenverstand« und sorgfältigem Analysieren der Situation beruhen (»semiformale Ansätze«).

Maßnahmen gegen einen aktiven Angriff

(gegen den Mann in der Mitte)

• Vorherige gegenseitige Authentisierung der Teilnehmer. Achtung: Kann M sich in hängende Verbindungen einschalten? D. h. in bereits authentisierte?
• Erweiterung des Protokolls, hier etwa durch Zertifikate (weiterer Mitspieler: N). Achtung: Kooperation von M mit N? N tritt selbst als M auf?
• Zusätzliche Synchronitätsforderungen -
  • z. B. künstliches Aufspalten von Nachrichten (Interlock-Protokoll),
  • Zeitstempel,
  • parallele Kommunikationskanäle.

• Starke Ressourcen nötig,
• hohes Entdeckungsrisiko.

Ansätze zur verfeinerten Modellierung

Modellierung von M (formal komplizierter als für E). Evtl. »Vernichten von Daten« modellieren.

Zusätzlich ins Modell einbauen:

• »Wissen«: A ist sicher, dass m korrekt ist,
• evtl. probabilistisch (»Glauben«).

Modellierung von »Vertrauen«.

Differenzierung von Angreifern nach Motiven, Absichten und Fähigkeiten.

Noch manches lässt sich modellieren. Das Problem dabei ist,

• das Modell handhabbar zu halten,
• d. h. so, dass sich noch etwas damit anfangen lässt.

Schwierigkeiten bei Modellierung und Sicherheitsnachweis

• Stimmen die Grundannahmen und Randbedingungen des Protokolls?
  • Sind z. B. die kryptographischen Mechanismen sicher?
  • Sind die Grundannahmen und Randbedingungen des Protokolls vollständig?
  • Erleichtert das Protokoll die Kryptoanalyse der Grundfunktionen? (z.  durch Nichteinhaltung von Zufallsanforderungen, Einschränkung des Suchraums)
  • 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? Sind seine Möglichkeiten vollständig erfasst? 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 möglich? Auch mit statistischen Methoden?
• Verdeckte Kanäle?

Formale Analyse kryptographischer Protokolle (Übersicht)

(Auch bekannt als »formalisierte Paranoia«.)

A. D. Rubin/ P. Honeyman: Formal methods for the analysis of authentication protocols. http://www.citi.umich.edu/techreports/reports/citi-tr-93-7.pdf

Klassifikation der Methoden nach Catherine Meadows:

1. Allgemeine Spezifikationssprachen und Verifikationsmethoden.
2. Expertensysteme, die verschiedenen Szenarien analysieren.
3. Logik von Wissen und Glauben formalisieren.
4. Algebraische Termersetzungen in kryptographischen Systemen.

Praktikable Ansätze zur Realisierung:

• Beweis-Analyse (proof checker) - ein vom Nutzer vorgegebener Sicherheitsbeweis wird auf Fehler untersucht.
• Modell-Analyse (model checker) - sämtliche Zustände des Systems (als endlicher Automat modelliert) werden auf Zulässigkeit überprüft.

Probleme der formalen Analyse

Keine Methode führt zu einem vollständigen formalen Sicherheitsbeweis.

Ausgewählte Probleme (nach Peter Gutmann):

• Formale Spezifikationen sind schwer verständlich, in der Regel sogar für den Autor. Daher ist kaum nachzuvollziehen, ob sie das tatsächlich gewünschte Systemverhalten korrekt modellieren.
• Auf formalen Spezifikationen basierende Beweise sind in der Regel fehlerhaft - wie alle mathematischen Beweise. (Die Sicherheit, mit der mathematische Sätze geglaubt werden, kommt nicht aus vollständigen formalen Beweisen!)
• Formale maschinelle Beweise sind schon in einfachen Beispielen wegen hoher Komplexität nicht durchführbar.
• Der Übergang von einer formalen Spezifikation eines Protokolls zu einem endlichen Automaten kann selbst Fehler enthalten.
• Modell-Analyse scheitert an der kombinatorischen Explosion - es gibt zu viele verschiedene mögliche Zustände.
• Der Übergang von einer formalen Spezifikation zu ausführbarem Code ist keine äquivalente Umformung. Z. B. ist die Semantik der Spezifikationssprache nicht genau in der Implementationsprache abbildbar. [Typische Kritik am Java-Sicherheitsmodell]
• Nach dem formalen Beweis darf der Programm-Code nicht mehr geändert werden. Das ist ein völlig unrealistisches Modell des Software-Entwickungsprozesses. Z. B. wirft jede noch so kleine Code-Optimierung einen durchgeführten Beweis über den Haufen.
• Die Laufzeitumgebung eines Programms muss in die Analyse einbezogen werden.
• Durchgeführte, veröffentlichte formale Spezifikationen und Verifikationen steckten voller Fehler.
• Es gibt viele Beispiele, wo formale Methoden selbst triviale Fehler und Lücken nicht gefunden haben.
• Alles bisher Bewiesene war auch ohne Formalisierung zu sehen (zumindest danach).
• 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.
• Es gibt keine empirische Evidenz, dass formale Methoden sicherer oder effizienter sind als sorgfältiges strukturiertes Vorgehen.
• Die meisten Fehler werden immer noch durch ausgiebiges Testen gefunden.
• Ein formaler Sicherheitsbeweis ist Kunden nicht verständlich vermittelbar.
• Formale Verifikation sorgt nicht für »gute«, »nützliche« oder in irgendeinem Sinn »brauchbare« Software - nur für Konsistenz mit der Spezifikation. Verifizierte korrekte Software kann beliebig schlecht sein (das »ISO-9000«-Phänomen).
• Formale Methoden haben sich in der Software-Entwicklung nicht durchgesetzt. (Anders beim Chip-Design, aber das ist ein ziemlich andersartiger Problemkreis - Hardware hat kein Pointer, keine Endlosschleifen, keine Rekursion, keine dynamischen Datenstrukturen, ..., und die Reproduktion von Hardware ist teurer, also lohnt sich der Aufwand formaler Methoden eher.)

Was bleibt?

Nutzen für eng umgrenzte Teilprobleme - als Teil der Fehlersuche.

»Wie bei den meisten Verifikationstechniken liegt der Nutzen weitgehend in der Identifikation von Fehlern und weniger im Nachweis, dass alles perfekt ist.« (Peter G. Neumann)

Weiterführende Literatur

Ross Anderson: Why cryptosystems fail. Communications of the ACM 37 (1994), 32 - 40. [online im WWW unter http://www.cl.cam.ac.uk/users/rja14/wcf.html]

Peter G. Neumann: Architectures and Formal Representations for Secure Systems. Final Reprot SRI Project 6401, 1995. [online im WWW unter http://www.csl.sri.com/papers/csl-96-05/]

BSI-Projekt Formale Methoden.

Bruce Schneier: Why cryptography is harder then it looks. Security Bulletin 2/2 (1997), 31 - 36. [online im WWW unter http://www.counterpane.com/whycrypto.html]

Bruce Schneier, Adam Shostack: Breaking up is hard to do: Modeling security Threats for smart cards. 1999. [online im WWW unter http://www.counterpane.com/smart-card-threats.html]

Ken Thompson: Reflections on trusting trust. Communications of the ACM 27 (1984), 761 - 763. [online im WWW unter http://www.acm.org/classics/sep95/]

Committee on Information Systems Trustworthiness, National Research Council: Software for Networked Information Systems. [online im WWW unter http://www.nap.edu/readingroom/books/trust/trust-3.htm], Kapitel 3 des Buchs Trust in Cyberspace.

Peter Gutmann: The Design and Verification of a Cryptographic Security Architecture (Dissertation). [online im WWW unter http://www.cs.auckland.ac.nz/~pgut001/pubs/thesis.html], .

Das beinahe enzyklopädische Verzeichnis von kryptographischen Protokollen aller Art ist die »Applied Cryptography« von Bruce Schneier, siehe das Literaturverzeichnis.

Helger Lipmaa hat eine umfangreiche Liste mit Links zum Thema »Authentication Logic«, wo man auch viele formale Verifikationsansätze findet.