Kryptographisch korrekte Sicherheitsanalyse von kryptographischen Protokollen

• Antragsteller: Professor Dr. Michael Backes
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2006 bis 2011
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 27419139

Kryptographische Protokolle stellen die Grundlage sicherer und verbindlicher Kommunikation über elektronische Medien wie z.B. das Internet dar. Heutzutage ist es allgemein anerkannt, dass die Sicherheit kryptographischer Protokolle mathematisch bewiesen werden muss, um verlässliche Sicherheitsgarantien zu erhalten. Zwei unterschiedliche Ansätze existieren, um solche Beweise zu führen: Der kryptogmphische Ansatz garantiert umfangreiche Sicherheitseigenschaften für realistische Protokollimplementierungen basierend auf Resultaten der zugrundeliegenden kryptographischen Algorithmen and komplexitätstheoretischen Annahmen. Der formale-Methoden Ansatz überlässt die langwierigen und fehleranfälligen Teile der Beweise maschinellen Verifikations-Werkzeugen und erlaubt daher fehlerunanfälligere, glaubwürdigere Beweise selbst komplexer Protokolle basierend auf Idealisierungen der Kryptographie. Gegenstand des Vorhabens ist die Untersuchung von Gemeinsamkeiten und Unterschieden der beiden Ansätze. Die Gemeinsamkeiten sollen vorteilhaft verbunden werden mit dem Ziel, maschinell verifizierte Beweise mit umfangreichen, kryptographisch fundierten Sicherheitsgarantien von Sicherheitsprotokollen zu erhalten. Das Vorhaben umfasst insbesondere komplexe Sicherheitseigenschaften kryptographischer Protokolle wie z.B. komplexe Geheimhaltungseigenschaften, Sicherheitsanalysen im Rahmen von komplexen System- und Angreifermodellen wie z.B. dynamische reaktive Systemmodelle bzw. dynamische Korrumpoierung ehrlicher Protokollteilnehmen durch den Angreifer, sowie die Entwicklung von effizienten, kryptographisch fundierten Verifikations-Werkzeugen. Die Herausarbeitung der Unterschiede der beiden Ansätze hat die Erlangung von Unmöglichkeitsresultaten zum Ziel, d.h. die Entdeckung und Erforschung von Protokollklassen, für die kein generelles kryptographisches Korrektheitsresultat erzielt werden kann.

• DFG-Verfahren: Sachbeihilfen