Automatische Verifikation kryptographischer Protokolle

点击翻译按钮获取中文摘要

Kryptographische Protokolle bilden die Basis für Anwendungen, die auf sichere Kommunikation angewiesen sind. Beispiele derartiger Anwendungen sind Online-Banking und -Shopping sowie elektronische Kreditkartentransaktionen. Da die Entwicklung sicherer kryptographischer Protokolle äußerst fehleranfällig ist, ist eine formale Analyse solcher Protokolle unerlässlich. Die bisher entwickelten Methoden und Werkzeuge zur Analyse kryptographischer Protokolle sind jedoch meist nur auf einfache Authentifizierungs- und Schlüsselaustauschprotokolle anwendbar; insbesondere stehen nur für diese einfachen Protokolle Algorithmen zur automatischen Verifikation zur Verfügung. Das wesentliche Ziel dieses Forschungsvorhabens ist es deshalb, Modelle und Algorithmen zur automatischen Verifikation kryptographischer Protokolle, die mit bisherigen Methoden nicht oder nur bedingt gehandhabt werden können, zu entwickeln und zu untersuchen. Dabei liegt das Hauptaugenmerk meiner Arbeit auf Schlüsselaustausch- und Authentifizierungsprotokollen mit komplexen Datenstrukturen, welche insbesondere Gruppenprotokolle einschließen, sowie fairen Austauschprotokollen, die E-Commerce-Protokolle umfassen.