Develop and mechanize a multi-modal logic (based on the awareness and belief of agents) for specifying and analyzing protocols and their properties

• Antragsteller: Professor Dr. David Basin
• Mitantragsteller: Dr. Luca Viganò
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2002 bis 2005
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5392968

Sicherheitsprotokolle spielen eine zentrale Rolle in der Sicherheit von verteilten Systemen und deren Anwendungen. Obwohl sie auf den ersten Blick einfach erscheinen, stellen Entwurf und Verifikation von Sicherheitsprotokollen eine große Herausforderung in der Informatik und den formale Methoden dar. Es gibt zwar bereits verschiedene Ansätze zur Analyse von Sicherheitsprotokollen, jedoch gibt es bislang keine Methode, die (i) eine geeignete semantische Grundlage bietet, (ii) in der Sicherheitseigenschaften einfach zu formalisieren sind, und (iii) mit der die Verifikation von Sicherheitseigenschaften oder das Entdecken von Sicherheitslücken unterstützt werden. In diesem Projekt werden wir eine multimodale Logik entwickeln, welche die Verwirklichung aller drei Forderungen durch die Kombination sich ergänzender Techniken aus den Bereichen Sicherheitslogik, Theorembeweisen und Modellprüfverfahren anstrebt. Ein Hauptmerkmal unseres Ansatzes wird die Fundierung der Logik auf dem Konzept der awareness sein. Dieses Konzept wird uns bei der Spezifikation und Analyse von Sicherheitseigenschaften unter Berücksichtigung eines Modells der verzahnten Protokolldurchläufe behilflich sein. Wir werden diese Logik in einem Theorembeweiser mechanisieren und für die Analyse komplexer, wirtschaftlich relevanter Protokolle (wie z.B. die Protokolle, die von der Internet Engineering Task Force vorgeschlagen werden) verwenden.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Schweiz