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 Werkzeug formalisiert und die DY basierte Analyse eingebettet werden. Durch die integrierte Verifikationstechnik für Protokolle wird die Lücke zwischen komplementären Analysemethoden geschlossen.
Bei der Implementierung ergeben sich durch die Verfeinerung des abstrakten Protokollmodells neue Angriffsmöglichkeiten. Neben der adäquaten Realisierung der kryptographischen Primitive müssen diese bei der Implementierung der Protokollregeln zusätzlich zur klassischen Korrektheit berücksichtigt werden. In ProtoTo soll für die genannten Verfeinerungsaspekte ein Modell geschaffen werden, das insbesondere auf existierende Techniken der Codeverifikation zurückgreift.
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 den Vertrauenswürdigkeitsstufen der Common Criteria (CC) abgestuften durchgängigen 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.
Partner
Kobil Systems GmbH, Sirrix AG, Technische Universität Darmstadt
