In den letzten Monaten habe ich die verschiedenen Forschungsbereiche, die in meinem PhD Projekt relevant sind, vorgestellt. Nun setze ich die Bausteine zusammen und stelle einen großen Meilenstein meiner Arbeit vor: CheckMate. Um den Nutzen und die Funktionsweise von CheckMate zu verstehen, fangen wir nochmal von vorne an.

Blockchain ist eine Technologie die uns Konzepte wie Kryptowährungen ermöglicht. Auf der Basis solcher unfälschbaren Währungsdaten, die festhalten wer wie viel dieser Währung besitzt, können wie bei konventionellen Währungen auch Geschäfte wie z.B. Überweisungen gemacht werden. Detaillierte Erklärungen dazu gibt es in meinem Blog "Was, Wie, Wofür Blockchain?". Blockchain Technologie kann aber viel mehr als einfache Transaktionen zu bewerkstelligen: Man kann diverse Finanzprodukte wie Crowd Funding, Auktionen oder Glücksspiel umsetzen. Diese komplexeren Anwendungen basieren auf sogenannten Smart Contracts oder auch Protokollen.

Solche Protokolle sollten sicher sein. Das heißt ein Hacker*innenangriff sollte unmöglich sein. Um das sicherzustellen müssen beide Aspekte eines solchen Protokolls berücksichtigt werden: die Kryptographischen und die Spieltheoretischen. Nehmen wir als Beispiel ein Passwort beim Online Banking: Dass das Passwort beim Eingeben geheim bleibt, ist Kryptographie; dass man es nicht freiwillig jemandem weitergibt, ist Spieltheorie.

Nachdem es zur Analyse der kryptographischen Aspekte schon solide Forschungsergebnisse gibt, beschäftige ich mich mit den spieltheoretischen. Insbesondere möchte ich garantieren, dass sich einerseits niemand zu Unrecht bereichern kann und andererseits, dass ehrlichen Nutzer*innen kein Schaden entstehen kann. Diese beiden Eigenschaften habe ich im Blog "Das Spiel des Lebens" genauer erklärt.

In unserem Prototypen CheckMate haben wir diese Sicherheitseigenschaften zuerst in spieltheoretische Konzepte und in einem zweiten Schritt in logische Formeln übersetzt. Wie im Blog "Steht der Bauer im Zimmer,.." erörtert, kann man logische Formeln einem Automated Reasoner geben. Dieser kann einem sagen, ob es möglich ist, diese Formeln alle gleichzeitig zu erfüllen. Wenn man die Formeln auf eine gewisse Art bereitstellt, kann man aus dem Output des Automated Reasoners ableiten, ob die Sicherheitseigenschaften erfüllt sind oder nicht.

Unser Tool ist folgendermaßen aufgebaut.

Um die Darstellung besser zu veranschaulichen, nehmen Sie an, Sie besitzen z.B. Bitcoin und möchten an einer Auktion teilnehmen. Sie vertrauen der Anbieterin der Auktion nicht und möchten sich daher vergewissern, dass die Durchführung mit rechten Dingen zugeht. Dafür können Sie CheckMate verwenden.

Sie nehmen die Beschreibung der Auktion zur Hand (Protokoll) und wissen wie sie laut Anbieterin ablaufen sollte (ehrliches Verhalten). Dann modellieren Sie das Protokoll als Spiel und das ehrliche Verhalten als ehrliche Historie, was zugegebenermaßen nicht ganz einfach ist und Fachwissen bedarf. Das ist Schritt 1 in der obigen Darstellung. Den Rest übernimmt CheckMate. CheckMate übersetzt das Spiel mit der zugehörigen ehrlichen Historie in logische Formeln (Schritt 2) und gibt diese an einen Automated Reasoner weiter (Schritt 3). Der Automated Reasoner wiederum teilt CheckMate mit, ob die Formeln unerfüllbar (Schritt 4a) oder erfüllbar (Schritt 4b) sind. CheckMate kann daraus schließlich folgern, ob das ursprüngliche Protokoll sicher war oder nicht. Somit wissen Sie, ob Sie ruhigen Gewissens an der Auktion teilnehmen können.   

Wir haben CheckMate erfolgreich an bestehenden Protokollen getestet und unsere Ergebnisse bei einer Fachkonferenz eingereicht. Auf die Publikation kann man hier zugreifen. Unser Prototyp ist Open Source und kann unter https://github.com/apre-group/checkmate downgeloadet werden.

In der Zukunft haben wir vor an der Modellierung der Protokolle als Spiele zu feilen um den Zugang und die User*innenfreundlichkeit von CheckMate zu verbessern.