Hintergrund: Das Projekt ist Teil des Arbeitsprogramms des Bundesministeriums für Bildung und Forschung (BMBF) zur IT-Sicherheitsforschung, speziell „Schutz von Internet-Infrastrukturen; Technologien zur Angriffsprävention und Frühwarnung“.

Inhalt: Im akademischen Bereich existieren zahlreiche Ansätze zur Analyse der logischen Korrektheit von Sicherheitsprotokollen. Computerunterstütze Ansätze basieren durchweg auf dem Dolev-Yao (DY) Modell, das perfekte Kryptographie unterstellt. Auf der anderen Seite liegen Protokollbeweise im Rahmen von Modellen, die schwächere und komplexitätstheoretische Annahmen ermöglichen, bis heute (nur) als „Papierbeweise“ (paper and pencil) vor. In ProtoTo soll ein solches Modell im VSE Wekzeug formalisiert und die DY basierte Analyse eingebettet werden. Durch die integrierte Verifikationstechnik für Protokolle wird die Lücke zwischen komplementären Analysemethoden geschlossen.

Um die Anwendung der in ProtoTo zu entwickelnden Verifikationstechniken und entsprechenden Werkzeuge durch geschulte aber nicht unbedingt wissenschaftliche Benutzer zu ermöglichen, sollen Handlungsempfehlungen erstellt werden. Diese werden im Rahmen einer nach der Vertrauenswürdigkeitsstufen der Common Criteria (CC) abgestufte durchgängige Vorgehensweise zur Entwicklung von Protokollen definiert werden. Das Vorgehensmodell beinhaltet auch Vorgaben zu CC-Artefakten und ihrer Evaluierung. Es soll an zwei Fallstudien aus den Bereichen Trusted Computing Anwendungen und Sichere Software Updates evaluiert und dargestellt werden.

Projektpartner: DFKI GmbH (Koordinator), Kobil Systems GmbH, Sirrix AG.

Mitarbeiter: Özgür Dagdelen