Saarbrücker Informatiker für Forschung an Sicherheitsprotokollen ausgezeichnet

Für seine Arbeit „Towards an Automatic Analysis of Security Protocols in First-Order Logic“ aus dem Jahr 1999 hat Christoph Weidenbach nun den Thoralf-Skolem-Preis erhalten.

2,93 Billionen US-Dollar wurden 2018 weltweit im Online-Einzelhandel umgesetzt. Sogenannte Sicherheitsprotokolle bilden dafür das Fundament. Christoph Weidenbach, Informatik-Professor der Saar-Universität und Leiter einer Forschungsgruppe am Max-Planck-Institut für Informatik, hat bereits 1999 dazu einen wissenschaftlichen Beitrag geleistet, für den er nun mit dem internationalen Thoralf-Skolem-Preis ausgezeichnet wurde. Diese Forschung ist heute eine der Grundlagen für digitale Kurznachrichten, deren Versand mit speziellen Programmen abgesichert wird. Mit ihrer Hilfe verständigen sich zwei Computer und stellen durch Verschlüsselung sicher, dass niemand die Kommunikation mitlesen kann.

Sicherheitsprotokolle werden auch heute noch von Menschen entworfen. „Allerdings haben die letzten 30 Jahre gezeigt, dass Menschen die Phantasie fehlt, wie man diese Protokolle knacken kann“, erklärt Christoph Weidenbach, der die Forschungsgruppe „Automatisierung der Logik“ am Max-Planck-Institut für Informatik in Saarbrücken leitet. Daher setzte man dazu Computer ein, die durch systematisches Überprüfen am Ende nachweisen können, dass das Protokoll wirklich sicher ist. Als grundlegende Arbeiten zu dieser automatischen Analyse von Sicherheitsprotokollen gelten die Forschungsergebnisse von Catherine Meadows, Naval Research Laboritory, Washington, USA, Larry Paulson, University of Cambridge, Großbritannien und Weidenbach. Alle wurden Ende der 1990er Jahre publiziert.

Für seine Arbeit „Towards an Automatic Analysis of Security Protocols in First-Order Logic“ aus dem Jahr 1999 hat Weidenbach den Thoralf-Skolem-Preis erhalten. Diese Auszeichnung ist ein sogenannter „test-of-time“ Preis. Er wird während der „Conference on Automated Deduction“, kurz CADE, der führenden, internationalen Konferenz auf dem Gebiet des maschinellen Beweisens, verliehen. Das Besondere: Die internationale Jury zeichnet damit kein aktuelles Forschungsergebnis aus, sondern den Einfluss der veröffentlichten Arbeit auf das Gebiet des maschinellen Beweisens in den vergangenen zehn Jahren.

Insbesondere zwei Aspekte von Weidenbachs Arbeit lobte die Jury: Der Aufsatz beschrieb erstmals, wie man Techniken des maschinengestützten Beweisens auf Sicherheitsprotokolle für den Schlüsselaustausch anwenden kann. Zudem lieferte Christoph Weidenbach darin neue Ergebnisse zur Entscheidbarkeit und Unentscheidbarkeit von so genannten Horn-Formeln, die zur Beschreibung von Sicherheitsprotokollen, aber auch von Programmen im Allgemeinen, eine wichtige Rolle spielen.

Damit erhält Weidenbach nach 2017 bereits zum zweiten Mal den Thoralf-Skolem-Preis. Dieser Preis wird seit 2014 vergeben und geht an Wissenschaftlerinnen und Wissenschaftler, die ihre Forschungsergebnisse auf der Konferenz präsentierten und damit in den vergangenen 10, 20, 30, 40 Jahren das Forschungsgebiet geprägt haben. Als Namensgeber dient der norwegische Mathematiker Albert Thoralf Skolem, der bereits aufgrund seiner Doktorarbeit 1926 so viel Beachtung fand, dass sogar der norwegische König davon erfuhr. Neben philosophischen Schriften schuf Skolem die mathematischen Grundlagen, die heute mit das Fundament der Computerwissenschaften bilden.

Weitere Informationen:
Über den Thoralf Skolem Award: http://cadeinc.org/Skolem-Award

Pressefoto unter: www.uni-saarland.de/pressefotos

Fragen beantwortet:
Professor Christoph Weidenbach
Universität des Saarlandes
Saarland Informatics Campus E1.4
Tel.: 0681 9325 900
E-Mail: weidenbach@mpi-inf.mpg.de

Redaktion:
Gordon Bolduan
Kompetenzzentrum Informatik Saarland
Universität des Saarlandes
Saarland Informatics Campus E1.7
Tel.: 0681/302-70741
E-Mail: bolduan@mmci.uni-saarland.de