2006-2007 AVISPA

Ziel des AVISPA-Projekts ist es, der Öffentlichkeit eine industriell einsetzbare Plattform zur automatischen Validierung sicherheitsrelevanter Kommunikationsprotokolle zur Verfügung zu stellen. Für die Verifikation wird das Protokoll zunächst in der Hochsprache HLPSL modelliert. Ein Compiler übersetzt die Spezifikation dann in ein maschinell weiterverarbeitbares Format, das sogenannte IF-Format. Jetzt kann das Protokoll mit verschiedenen Werkzeugen überprüft werden. Bei der Prüfung kommen hauptsächlich Modell-Checker zum Einsatz.

Dr. Heinrich Hördegen hat verschiedene Module für den Compiler des AVISPA-Projekts entwickelt. Entwicklungssprache war Objective Caml, eine funktionale Programmiersprache. Zusätzlich hat er Teile einer Web-Oberfläche entwickelt, die es erlaubt, interaktiv Kommunikationsprotokolle zu verifizieren. Dr. Heinrich Hördegen hat mehrere Schriften zu Fragen der IT-Sicherheit veröffentlicht.

Das internationale Projekt war eine Zusammenarbeit der Universität Genua, der ETH Zürich, des LORIA und der Siemens AG. Es wurde von der europäischen Kommission finanziert.

 

Ausgewählte Publikationen

Explicit Randomness is not Necessary when Modeling Probabilistic Encryption

 

Pseudo-Random Generator Based on Chinese Remainder Theorem