Automatische Analyse kryptographischer Protokolle mit komplexen Nachrichtenformaten

• Antragsteller: Professor Dr. Ralf Küsters
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2005 bis 2011
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5445829

• Erstellungsjahr: 2011

Zusammenfassung der Projektergebnisse

Generelles Ziel des Vorhabens war es, für kryptographische Protokolle mit komplexen Nachrichtenformaten geeignete Modelle für deren Analyse zu entwerfen und die Protokolle auf Basis dieser Modelle einer automatischen Analyse zugänglich zu machen bzw. die Grenzen einer solchen Analyse – im Sinne von Entscheidbarkeit, Komplexität und Praktikabilität – zu untersuchen, wobei der Schwerpunkt auf Gruppen- und Web-Service-Protokollen liegen sollte. Neben symbolischen Analysen im sogenannten Dolev-Yao-Modell waren auch kryptographische Modelle und Analysen Gegenstand des Projektes. Für die automatische Analyse von Gruppenprotokollen existierten zu Anfang des Projektes fast keine Resultate, geschweige denn praktikable Analyseverfahren. Durch das Projekt konnte der diesbezügliche Stand der Forschung deutlich vorangebracht werden. Unter anderem wurden, basierend auf einem Logikprogrammierungansatz, praktikable Analyseverfahren für Protokolle entwickelt, die häufig anzutreffende Operatoren, wie das exklusive Oder und die Diffie-Hellman-Exponentiation verwenden. Unsere Arbeiten lösten damit ein offenes Problem im Bereich der automatischen Analyse kryptographischer Protokolle, auch über die Frage der Analyse von Gruppenprotokollen hinaus, und zeigte neue Perspektiven und Techniken auf. Die Verfahren konnten dabei nicht nur auf Protokolle, einschließlich Gruppenprotokolle und Internetstandards, angewendet werden, sondern auch auf eine bestimmte Klasse sogenannter Sicherheits-APIs, einschließlich eines in Bankautomaten verwendeten Hardware-Sicherheitsmoduls, für das durch unsere automatische Analyseverfahren ein bisher unbekannter Angriff offengelegt wurde. Unsere Verfahren wurden darüberhinaus bereits von anderen Wissenschaftlern für die automatische Analyse von RFID-Protokollen verwendet. Im Bereich der in der Praxis weit verbreiteten Web-Service-Protokolle haben wir auf Basis der in den Standards zu Web Services vorgesehenen Sicherungsmechanismen und gemäß der gängigen Praxis verschiedene Basisprotokolle identifiziert und diese erstmals einer rigorosen kryptographischen Analyse unterzogen. Dabei ist es gelungen, verschiedene für Web-Service-Protokolle spezifische Merkmale zu berücksichtigen. Dazu zählen die Request-Response-Struktur, komplexe Nachrichtenformate, die Verwendung von Zeitstempeln und langlebige, nicht gegen temporäre Ausfälle gefeite Server. Die Ergebnisse bilden eine solide Grundlage für die Implementierung sicherer Web-Service-Protokolle.

Projektbezogene Publikationen (Auswahl)

• Implementing a Unification Algorithm for Protocol Analysis with XOR. In: 20th International Workshop on Unification (UNIF 2006), 2006
  M. Tuengerthal, R. Küsters, and M. Turuani
  
• On the Automatic Analysis of Recursive Security Protocols with XOR. In: Proceedings of the 24th Symposium on Theoretical Aspects of Computer Science (STACS 2007), S. 646–657, Lecture Notes in Computer Science, Bd. 4393, Springer, 2007
  R. Küsters, T. Truderung
  
• Selecting Theories and Nonce Generation for Recursive Protocols. In: Proceedings of the 5th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE 2007), S. 61–70, ACM Press, 2007
  K. O. Kürtz, R. Küsters, Th. Wilke
  
• Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach. In: Proceedings of the 2008 ACM Conference on Computer and Communications Security (CCS 2008), S. 129–138, ACM Press, 2008
  R. Küsters, T. Truderung
  
• A Simulation-Based Treatment of Authenticated Message Exchange. In: Proceedings of the 14th Asian Computing Science Conference (ASIAN 2009), S. 109–123, Lecture Notes in Computer Science, Bd. 5913, Springer, 2009
  K. O. Kürtz, H. Schnoor, Th. Wilke
  
• Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF 2009), S. 157–171, IEEE Computer Society, 2009
  R. Küsters, T. Truderung
  
• Computationally Secure Two-Round Authenticated Message Exchange. In: Proceedings of the 2010 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2010), S. 214–225, ACM Press, 2010
  K. O. Kürtz, H. Schnoor, Th. Wilke
  
• Secure Two-Round Message Exchange. Dissertation, Universität Kiel, 2010
  K. O. Kürtz
  
• Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach. Journal of Automated Reasoning, 46(3):325–352, 2011
  R. Küsters and T. Truderung