Automatische Analyse kryptographischer Protokolle mit komplexen Nachrichtenformaten

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

Grundlage sicherer und verbindlicher elektronischer Kommunikation und der elektronischen Abwicklung von Geschäftsvorgängen sind kryptographische Protokolle (bzw. Protokolle mit kryptographischen Anteilen). Deren Entwurf ist erfahrungsgemäß sehr schwierig und stark fehleranfällig, weshalb eine automatische Analyse unabdingbar ist. Gegenstand der Untersuchungen des Vorhabens sind kryptographische Protokolle, die sich dadurch auszeichnen, dass die bei ihrer Ausführung ausgetauschten Nachrichten von komplexen Beschaffenheit sind. Dies ist zum Beispiel der Fall bei Web-Service-Protokollen: eine Nachricht kann hier unter anderem verschlüsselte Bestell- und Preisangaben, signierte und damit authentifizierte Routingvorgaben und Firewall- Zertifikate enthalten. Ein anderes Beispiel sind Multicasting- Protokolle. Derartige Protokolle lassen sich mit der bislang entwickelten Theorie nicht automatisch analysieren. Ziel der Untersuchungen ist es deshalb, für solche Protokolle geeignete Modelle zu entwerfen, effiziente Verfahren zur automatischen Analyse dieser Protokolle zu entwickeln und die Grenzen ihrer automatischen Analyse aufzuzeigen.