Werkzeugbasierte Verifikation von Sicherheitsprotokollen mit einem kombinierten typ- und trace-basierten Ansatz

• Antragsteller: Professor Dr. Ralf Küsters
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 557128350

Sicherheitsprotokolle sind unerlässlich für sichere Kommunikation, die Gewährleistung der Privatsphäre und Datenintegrität sowie für Authentifizierungs- und Autorisierungsaufgaben und bilden den Kern nahezu aller sicherheitskritischer Anwendungen. Sie sind meist komplex und ihr Entwurf extrem fehleranfällig, weshalb eine informelle Beurteilung der Sicherheit solcher Protokolle leicht Angriffe und Schwachstellen übersieht. Die Analyse von Sicherheitsprotokollen erfordert daher einen rigorosen formalen Ansatz. Das geplante Projekt konzentriert sich auf die sogenannte symbolische Analyse, die bereits erfolgreich für die formale Analyse weit verbreiteter Protokolle aus der Praxis eingesetzt wurde, darunter TLS, EMV, FIDO, 5G und Signal. Diese Analysen haben Angriffe aufgedeckt, die zu Protokollverbesserungen und anschließenden Sicherheitsbeweisen geführt haben. Trotz dieser Erfolge stehen automatisierte Werkzeuge zur symbolischen Analyse weiterhin vor vielen Herausforderungen, vor allem entlang der Dimensionen Skalierbarkeit, Automatisierung und Ausdruckskraft. Symbolische Protokollanalysewerkzeuge werden üblicherweise in trace- und typbasierte Ansätze unterteilt. Erstere konzentrieren sich vor allem auf Automatisierung, arbeiten mit abstrakten Modellierungssprachen und untersuchen große Teile von Protokollen auf einmal, während typbasierte Werkzeuge mehr manuelle Arbeit erfordern, allerdings eine feingranulare Protokollbeschreibung erlauben und es ermöglichen, einzelne Protokollschritte unabhängig voneinander zu analysieren, wodurch eine gute Skalierbarbeit erreicht wird. Der Antragsteller hat jüngst, zusammen mit Kollegen, einen neuen Ansatz zur werkzeugbasierten Analyse von Sicherheitsprotokollen vorgeschlagen, genannt DY*. DY* kombiniert trace- und typbasierte Ansätze mit dem Ziel, von beiden Welten zu profitieren. In DY* können Protokolle in der Programmiersprache F* geschrieben und analysiert werden, was präzise und ausführbare Protokollmodelle ermöglicht. Darüberhinaus nutzt DY* das reichhaltige Typsystem von F* für die modulare und unabhängige, und somit skalierbare, Verifikation einzelner Protokollschritte, bietet dabei, anders als rein typbasierte Ansätze, allerdings eine klare Semantik ähnlich zu trace-basierten Ansätzen. Dieses Projekt zielt nun darauf ab, das DY*-Framework und seinen neuartigen Ansatz, welcher Vorteile bisher getrennter Analyseansätze kombiniert, in den drei Dimensionen Skalierbarkeit, Automatisierung und Ausdruckskraft weiter voranzutreiben und DY* als ein leistungsfähiges und vielseitiges neues Werkzeug für die Verifikation von Sicherheitsprotokollen zu etablieren. Mit den im Rahmen dieses Projektes entwickelten Verbesserungen ist zudem geplant, Fallstudien zu wichtigen, weit verbreiteten Protokollen und Standards aus der Praxis durchzuführen, welche von unabhängigem Interesse sind.

• DFG-Verfahren: Sachbeihilfen