Sicherer Schlüsselaustausch

Internets, haben Sicherheitsaspekte von verwendeten Diensten stark an
Bedeutung gewonnen und machen den Einsatz kryptographischer Primitive
und Protokolle unumgänglich. Da kryptographische Systeme fast immer
die Verfügbarkeit gemeinsamer kryptographischer Schlüssel erfordern,
ist speziell der sichere Schlüsselaustausch einer der grundlegendsten
Sicherheitsdienste, auf dem alle weiteren Mechanismen aufbauen. Die
Beweisbarkeit der Sicherheit solcher Systeme ist dabei von eminenter
Wichtigkeit: Ohne Sicherheitsbeweise lässt sich die Verlagerung
kritischer Dienste wie Geld-Transaktionen und Transfer von
medizinischen Daten auf offene Netze nicht rechtfertigen.

Zum Sicherheitsbeweis existieren zwei klassische Ansätze: (1) formale
Methoden basierend auf Term-Algebren zur Abstraktion von
kryptographischen Primitiven und (2) komplexitätstheoretische
Betrachtungen im Sinne moderner Kryptographie. Beide weisen jedoch
Schwachstellen auf und sind dadurch nicht zufriedenstellend.

In diesem Vortrag werde ich diese Problematiken am Beispiel des
Schlüsselaustauschs illustrieren. Im weiteren stelle ich einen neuen
Ansatz vor, der die Vorteile beider Ansätze in sich vereint:
Einerseits erlaubt dieser Ansatz eine präzisere Modelierung der realen
Welt unter Berücksichtigung kryptographischer Annahmen und
Angreifer-Erfolgswahrscheinlichkeiten. Andererseits ermöglicht dieser
Ansatz die modulare Komposition von Abstraktionen, auf deren Basis auch
automatische Beweis-Tools operieren können.