Analyse kryptographischer Protokolle

Kryptographische Protokolle bilden die Grundlage für sichere elektronische Kommunikation und damit auch für sichere Geschäftstransaktionen. Der Entwurf kryptographischer Protokolle ist jedoch äußerst komplex und fehleranfällig, da diese Protokolle ihre Ziele auch unter der (realistischen) Annahme erreichen müssen, dass ein Angreifer das Kommunikationsnetzwerk kontrolliert und dass er Nachrichten aus mehreren Protokollsitzungen zwischen möglicherweise unehrlichen Parteien kombinieren kann. Deshalb ist eine systematische Analyse kryptographischer Protokolle unverzichtbar. Die bislang hierzu entwickelten Ansätze reichen von manuellen Methoden basierend auf komplexitätstheoretischen und probabilistischen Modellen bis hin zu automatischen symbolischen Verfahren.

Im Vortrag werde ich, nach einem Überblick über die verschiedenen Ansätze, genauer auf die symbolischen Verfahren eingehen, mit deren Hilfe bereits zahlreiche Fehler in veröffentlichten Protokollen gefunden wurden. Im Mittelpunkt des Vortrages werden dabei automatische Verfahren stehen, die über die Analyse einfacher Protokolle und Sicherheitsanforderungen hinausgehen. Als Beispiel betrachte ich dazu Verfahren zur Analyse von Protokollen, die häufig verwendete kryptographische Primitive, wie die Diffie-Hellman-Exponentiation, einsetzen. Zum Abschluss des Vortrages werde ich kurz die komplexitätstheoretischen und probabilistischen Modelle und ihre Beziehung zu den symbolischen Verfahren erläutern.