In dieser Arbeit präsentieren wir einen Ansatz, mit dem die Sicherheit von Protokollen für multi-party-computations (MPC) verbessert werden kann. Dafür gehen wir davon aus, dass Protokollteilnehmer aus mehreren Geräten mit unterschiedlicher Zusammensetzung von Hardware, Software und Betriebssystemen bestehen. Dies wird als diverse Redundanz bezeichnet. Dazu wird die Annahme getroffen, dass redundante Geräte aufgrund ihres unterschiedlichen Aufbaus nicht alle gleichzeitig korrumpiert werden können. Auf dieser Basis konstruieren wir ein MPC Protokoll, das sicher bleibt, selbst wenn die letzte ehrlich Partei teilweise korrumpiert wird. Um die Annahme formal zu beschreiben, schlagen wir ein Korruptionsmodell vor, das zwei unterschiedliche Typen von Korruptionen vorsieht. Um Angriffe über physikalischen Zugriff auf Geräte zu beschreiben, wird der übliche aktive Angriff benutzt. Angriffe über das Netzwerk werden jedoch eingeschränkt, um zu modellieren, dass solche Angriffe auf vorhandene Sicherheitslücken angewiesen sind. Wenn Systeme in diverser Redundanz vorliegen, ist es unwahrscheinlich, dass sie alle zur selben Zeit Sicherheitslücken aufweisen. Dieser Ansatz wird in der praktischen IT-Sicherheit bereits eingesetzt, wurde, so weit wir wissen, aber noch nicht verwendet, um formale Sicherheitsgarantien zu geben. Viele kryptographische Protokolle machen (implizit) die Annahme, dass jede Partei aus nur einem physikalischen Gerät besteht. Deshalb wird eine Partei dann entweder vollständig korrumpiert oder bleibt komplett ehrlich. Deshalb ist es für unsere Zwecke notwendig, Parteien in mehrere Geräte aufzuteilen. Diese Geräte führen dann ein Protokoll aus, mit dem eine ganze Partei realisiert wird. Um wichtige Stellen zu schützen, an denen die ganze Partei auf einmal korrumpiert werden könnte, setzen wir das MPC Protokoll SPDZ [Dam+13] ein. Hier nutzen wir aus, dass SPDZ nur innerhalb einer Partei eingesetzt wird. Hier vertrauen sich die Geräte, zumindest zu Beginn, bevor Korruptionen stattfinden können. Dieses initiale Vertrauen erlaubt es, den aufwändigsten Teil von SPDZ, die Vorverarbeitungsphase, zu überspringen. Dieser Ansatz verursacht linearen zusätzlichen Aufwand im Vergleich zu herkömmlichen Protokollen. Dafür wird sichergestellt, dass Parteien, die bis zu einem Viertel ihrer Geräte aufgrund von Korruptionen verlieren, weiter als ehrliche Parteien am Protokoll teilnehmen können. Außerdem bleibt ihre Ein- und Ausgabe geheim.
In dieser Arbeit präsentieren wir einen Ansatz, mit dem die Sicherheit von Protokollen für multi-party-computations (MPC) verbessert werden kann. Dafür gehen wir davon aus, dass Protokollteilnehmer aus mehreren Geräten mit unterschiedlicher Zusammensetzung von Hardware, Software und Betriebssystemen bestehen. Dies wird als diverse Redundanz bezeichnet. Dazu wird die Annahme getroffen, dass redundante Geräte aufgrund ihres unterschiedlichen Aufbaus nicht alle gleichzeitig korrumpiert werden können. Auf dieser Basis konstruieren wir ein MPC Protokoll, das sicher bleibt, selbst wenn die letzte ehrlich Partei teilweise korrumpiert wird. Um die Annahme formal zu beschreiben, schlagen wir ein Korruptionsmodell vor, das zwei unterschiedliche Typen von Korruptionen vorsieht. Um Angriffe über physikalischen Zugriff auf Geräte zu beschreiben, wird der übliche aktive Angriff benutzt. Angriffe über das Netzwerk werden jedoch eingeschränkt, um zu modellieren, dass solche Angriffe auf vorhandene Sicherheitslücken angewiesen sind. Wenn Systeme in diverser Redundanz vorliegen, ist es unwahrscheinlich, dass sie alle zur selben Zeit Sicherheitslücken aufweisen. Dieser Ansatz wird in der praktischen IT-Sicherheit bereits eingesetzt, wurde, so weit wir wissen, aber noch nicht verwendet, um formale Sicherheitsgarantien zu geben. Viele kryptographische Protokolle machen (implizit) die Annahme, dass jede Partei aus nur einem physikalischen Gerät besteht. Deshalb wird eine Partei dann entweder vollständig korrumpiert oder bleibt komplett ehrlich. Deshalb ist es für unsere Zwecke notwendig, Parteien in mehrere Geräte aufzuteilen. Diese Geräte führen dann ein Protokoll aus, mit dem eine ganze Partei realisiert wird. Um wichtige Stellen zu schützen, an denen die ganze Partei auf einmal korrumpiert werden könnte, setzen wir das MPC Protokoll SPDZ [Dam+13] ein. Hier nutzen wir aus, dass SPDZ nur innerhalb einer Partei eingesetzt wird. Hier vertrauen sich die Geräte, zumindest zu Beginn, bevor Korruptionen stattfinden können. Dieses initiale Vertrauen erlaubt es, den aufwändigsten Teil von SPDZ, die Vorverarbeitungsphase, zu überspringen. Dieser Ansatz verursacht linearen zusätzlichen Aufwand im Vergleich zu herkömmlichen Protokollen. Dafür wird sichergestellt, dass Parteien, die bis zu einem Viertel ihrer Geräte aufgrund von Korruptionen verlieren, weiter als ehrliche Parteien am Protokoll teilnehmen können. Außerdem bleibt ihre Ein- und Ausgabe geheim.
Moderne Kryptographie erlaubt nicht nur, personenbezogene Daten im Internet zu schützen oder sich für bestimmte Dienste zu authentifizieren, sondern ermöglicht auch das Auswerten einer Funktion auf geheimen Eingaben mehrerer Parteien, ohne dass dabei etwas über diese Eingaben gelernt werden kann (mit der Ausnahme von Informationen, die aus der Ausgabe und eigenen Eingaben effizient abgeleitet werden können). Kryptographische Protokolle dieser Art werden sichere Mehrparteienberechnung genannt und eignen sich für ein breites Anwendungsspektrum, wie z.B. geheime Abstimmungen und Auktionen. Um die Sicherheit solcher Protokolle zu beweisen, werden Annahmen benötigt, die oft komplexitätstheoretischer Natur sind, beispielsweise, dass es schwierig ist, hinreichend große Zahlen zu faktorisieren. Sicherheitsannahmen, die auf physikalischen Prinzipien basieren, bieten im Gegensatz zu komplexitätstheoretischen Annahmen jedoch einige Vorteile: die Protokolle sind meist konzeptionell einfacher, die Sicherheit ist unabhängig von den Berechnungskapazitäten des Angreifers, und die Funktionsweise und Sicherheit ist oft für den Menschen leichter nachvollziehbar. (Zum Beispiel forderte das Bundesverfassungsgericht: „Beim Einsatz elektronischer Wahlgeräte müssen die wesentlichen Schritte der Wahlhandlung und der Ergebnisermittlung vom Bürger zuverlässig und ohne besondere Sachkenntnis überprüft werden können.“ (BVerfG, Urteil des Zweiten Senats vom 03. März 2009)). Beispiele für solche Annahmen sind physikalisch getrennte oder unkorrumpierbare Hardware-Komponenten (vgl. Broadnax et al., 2018), Write-Only-Geräte für Logging, oder frei zu rubbelnde Felder, wie man sie von PIN-Briefen kennt. Auch die aus der Quantentheorie folgende Nicht-Duplizierbarkeit von Quantenzuständen ist eine physikalische Sicherheitsannahme, die z.B. verwendet wird, um nicht-klonbares „Quantengeld“ zu realisieren. In der vorliegenden Dissertation geht es neben Protokollen, die die Sicherheit und Isolation bestimmter einfacher Hardware-Komponenten als Vertrauensanker verwenden, im Besonderen um kryptographischen Protokolle für die sichere Mehrparteienberechnung, die mit Hilfe physikalischer Spielkarten durchgeführt werden. Die Sicherheitsannahme besteht darin, dass die Karten ununterscheidbare Rückseiten haben und, dass bestimmte Mischoperationen sicher durchgeführt werden können. Eine Anwendung dieser Protokolle liegt also in der Veranschaulichung von Kryptographie und in der Ermöglichung sicherer Mehrparteienberechnungen, die gänzlich ohne Computer ausgeführt werden können. Ein Ziel in diesem Bereich der Kryptographie ist es, Protokolle anzugeben, die möglichst wenige Karten benötigen – und sie als optimal in diesem Sinne zu beweisen. Abhängig von Anforderungen an das Laufzeitverhalten (endliche vs. lediglich im Erwartungswert endliche Laufzeit) und an die Praktikabilität der eingesetzten Mischoperationen, ergeben sich unterschiedliche untere Schranken für die mindestens benötigte Kartenanzahl. Im Rahmen der Arbeit wird für jede Kombination dieser Anforderungen ein UND-Protokoll – ein logisches UND zweier in Karten codierter Bits; dieses ist zusammen mit der Negation und dem Kopieren von Bits hinreichend für die Realisierung allgemeiner Schaltkreise – konstruiert oder in der Literatur identifiziert, das mit der minimalen Anzahl an Karten auskommt, und dies auch als Karten-minimal bewiesen. Insgesamt ist UND mit vier (für erwartet endliche Laufzeit (Koch, Walzer und Härtel, 2015; Koch, 2018)), fünf (für praktikable Mischoperationen oder endliche Laufzeit (Koch, Walzer und Härtel, 2015; Koch, 2018)) oder sechs Karten (für endliche Laufzeit und gleichzeitig praktikable Mischoperationen (Kastner et al., 2017)) möglich und optimal. Für die notwendigen Struktureinsichten wurden so-genannte „Zustandsdiagramme“ mit zugehörigen Kalkülregeln entwickelt, die eine graphenbasierte Darstellung aller möglichen Protokolldurchläufe darstellen und an denen Korrektheit und Sicherheit der Protokolle direkt ablesbar sind (Koch, Walzer und Härtel, 2015; Kastner et al., 2017). Dieser Kalkül hat seitdem eine breite Verwendung in der bereichsrelevanten Literatur gefunden. (Beweise für untere Schranken bzgl. der Kartenanzahl werden durch den Kalkül zu Beweisen, die zeigen, dass bestimmte Protokollzustände in einer bestimmten kombinatorischen Graphenstruktur nicht erreichbar sind.) Mit Hilfe des Kalküls wurden Begriffe der Spielkartenkryptographie als C-Programm formalisiert und (unter bestimmten Einschränkungen) mit einem „Software Bounded Model Checking“-Ansatz die Längenminimalität eines kartenminimalen UND-Protokolls bewiesen (Koch, Schrempp und Kirsten, 2019). Darüber hinaus werden konzeptionell einfache Protokolle für den Fall einer sicheren Mehrparteienberechnung angegeben, bei der sogar zusätzlich die zu berechnende Funktion geheim bleiben soll (Koch und Walzer, 2018), und zwar für jedes der folgenden Berechnungsmodelle: (universelle) Schaltkreise, binäre Entscheidungsdiagramme, Turingmaschinen und RAM-Maschinen. Es wird zudem untersucht, wie Karten-basierte Protokolle so ausgeführt werden können, dass die einzige Interaktion darin besteht, dass andere Parteien die korrekte Ausführung überwachen. Dies ermöglicht eine (schwach interaktive) Programm-Obfuszierung, bei der eine Partei ein durch Karten codiertes Programm auf eigenen Eingaben ausführen kann, ohne etwas über dessen interne Funktionsweise zu lernen, das über das Ein-/Ausgabeverhalten hinaus geht. Dies ist ohne derartige physikalische Annahmen i.A. nicht möglich. Zusätzlich wird eine Sicherheit gegen Angreifer, die auch vom Protokoll abweichen dürfen, formalisiert und es wird eine Methode angegeben um unter möglichst schwachen Sicherheitsannahmen ein passiv sicheres Protokoll mechanisch in ein aktiv sicheres zu transformieren (Koch und Walzer, 2017). Eine weitere, in der Dissertation untersuchte physikalische Sicherheitsannahme, ist die Annahme primitiver, unkorrumpierbarer Hardware-Bausteine, wie z.B. einen TAN-Generator. Dies ermöglicht z.B. eine sichere Authentifikation des menschlichen Nutzers über ein korrumpiertes Terminal, ohne dass der Nutzer selbst kryptographische Berechnungen durchführen muss (z.B. große Primzahlen zu multiplizieren). Dies wird am Beispiel des Geldabhebens an einem korrumpierten Geldautomaten mit Hilfe eines als sicher angenommenen zweiten Geräts (Achenbach et al., 2019) und mit möglichst schwachen Anforderungen an die vorhandenen Kommunikationskanäle gelöst. Da das angegebene Protokoll auch sicher ist, wenn es beliebig mit anderen gleichzeitig laufenden Protokollen ausgeführt wird (also sogenannte Universelle Komponierbarkeit aufweist), es modular entworfen wurde, und die Sicherheitsannahme glaubwürdig ist, ist die Funktionsweise für den Menschen transparent und nachvollziehbar. Insgesamt bildet die Arbeit durch die verschiedenen Karten-basierten Protokolle, Kalküle und systematisierten Beweise für untere Schranken bzgl. der Kartenanzahl, sowie durch Ergebnisse zur sicheren Verwendung eines nicht-vertrauenswürdigen Terminals, und einer Einordnung dieser in eine systematische Darstellung der verschiedenen, in der Kryptographie verwendeten physikalischen Annahmen, einen wesentlichen Beitrag zur physikalisch-basierten Kryptographie.
Depuis l'apparition de la cryptographie moderne, le calcul sécurisé (MPC) a longuement été étudié. Le MPC permet à un groupe de parties (ou joueurs) d'effectuer ensemble un ou plusieurs calculs sur des données secrètes, tout en garantissant que les joueurs n'obtiennent rien de plus que le résultat et ce qui peut en être déduit. Le développement massif de notre utilisation quotidienne d'Internet rend le besoin de méthodes de calcul sécurisé plus urgent que jamais : les calculs sur des données privées sont omniprésents, des algorithmes de recommandation aux enchères électroniques. Les algorithmes de MPC modernes bénéficient grandement de l'apport d'aléa corrélé, afin d'obtenir des protocoles rapides. Cet aléa corrélé doit être généré massivement au préalable pour que les protocoles de MPC puissent être efficaces. Toutefois, réaliser cette génération d'aléa corrélé efficacement reste encore un défi. Dans cette thèse, nous étudions les Générateurs de Corrélations Pseudo-aléatoires (PCGs). Cette primitive cryptographique transforme une petite quantité d'aléa corrélé en une large quantité de pseudo-aléa corrélé, tout en étant efficace en ce qui concerne le temps de calcul et la communication. Nous présentons différentes constructions de PCG dont la sécurité repose sur des variantes de l'hypothèse de Décodage de Syndrome (SD), une hypothèse classique en théorie des codes. L'intuition derrière les constructions proposées est de mélanger l'hypothèse SD avec certaines techniques de MPC qui permettent de partager de manière additive des vecteurs creux. Nos résultats obtenus battent l'état de l'art en ce qui concerne les protocoles de calcul sécurisé nécessitant plus de deux joueurs lorsque le calcul est effectué sur un corps fini de taille > 2. Nous montrons également comment supprimer cette contrainte au prix d'un léger surcoût en communication. Nous considérons également la construction de Fonctions Pseudo-aléatoires Corrélées (PCFs). Les PCFs produisent des corrélations à la volée : les joueurs détiennent chacun des fonctions corrélées de sorte que les sorties des fonctions, lorsqu'elles sont évaluées sur la même entrée, soient corrélées. Ces objets offrent plus de flexibilité que les PCGs, mais sont aussi plus difficiles à construire. Nous nous appuyons à nouveau sur des variantes de SD pour construire des PCFs. Nous nous basons sur une construction de PCF déjà établie, montrant que la preuve de sécurité associée était incorrecte, et proposons une correction. De plus, nous présentons des optimisations de la construction, provenant d'une meilleure analyse et d'un calcul précis des paramètres nécessaires via des simulations. Nous obtenons des paramètres utilisables en pratique. Cette thèse repose majoritairement sur l'hypothèse SD. La recherche d'une bonne complexité implique des efforts pour trouver les codes les plus efficaces tout en garantissant que la sécurité ne soit pas compromise. Nous considérons un modèle permettant l'étude de l'efficacité des attaques prometteuses contre SD et ses variantes. Pour chaque construction mentionnée précédemment, nous menons une analyse de sécurité approfondie de la variante associée de SD et tentons d'attaquer notre propre schéma pour calculer des paramètres concrets.
Privatsphärebewahrende authentifizierte Schlüsselaustauschverfahren (PPAKE, von engl. Privacy Preserving Authenticated Key Exchange) sind AKE (engl. Authenticated Key Exchange) Protkolle, die so konzipiert werden, dass sie die Identität der beiden Kommunikationspartner vor Dritten geheim halten. PPAKE Protokolle wurden bereits in der Vergangenheit betrachtet. In diesem Werk möchten wir die bestehenden formalen Privatsphäreeigenschaften solcher Protokolle stärken. Der wichtigste Zusatz ist, dass wir auch Angreifer betrachten, die den Protokollablauf nicht korrekt beenden (z.B. weil sie sich nicht authentifizieren können). Auch derartige Angriffe sind relevant, da es dem Angreifer möglicherweise egal ist, ob der Protkollablauf abgebrochen wird, nachdem er die Identität seines Zieles herausgefunden hat. Zusätzlich präsentieren wir ein formales Modell das diese Eigenschaften abbildet und mehrere Protkolle, die unterschiedlich starke Privatsphärebewahrungseigenschaften erfüllen. Eines davon ist eine genersiche Konstruktion aus generischen kryptografischen Grundbausteinen und kann daher auf eine Art instanziiert werden, von der angenommen wird dass sie selbst gegen zukünftige Quantencomputer sicher ist. Zudem präsentieren wir formale Beweise aller Protokolle in dem von uns eingeführten Modell. Der zweite Teil dieser Masterarbeit behandelt die automatische Verifikation der Privatsphäreeigenschaften des wichtigsten Protokolls aus dem ersten Teil. Automatische Verifikation wird verwendet, um entweder einen Angriff gegen ein Protokoll zu finden, oder festzustellen dass die angegebenen Eigenschaften tatsächlich erüllt sind. Dadurch wird die Wahrscheinlichkeit, in den von Menschenhand geschriebenen Beweisen einen Fehler gemacht zu haben, minimiert. Als erstes untersuchten wir die automatische Verifikationssoftware “Tamarin Prover”, die jedoch, bevor der zugeteilte Arbeitsspeicher von ca. 60 GB aufgebraucht war, zu keinem Ergebnis führte (weder einem Beweis noch einem Angriff). Daher nutzten wir stattdessen die Verifikationssoftware ProVerif und konnten die gewünschten Eigenschaften erfolgreich beweisen. In diesem Werk präsentieren wir sowohl unsere Tamarin- als auch unsere ProVerif-Formulierung.
Verschränkung ist nicht nur notwendig für die Beschreibung des Verhaltens von quantenmechanischen Systemen, sondern ist auch essentiell für einige vielversprechende Anwendungen der Quantenmechanik. Motiviert durch die Bedeutung von Verschränkung werden in dieser Arbeit Themen aus der Vielteilchenverschränkungstheorie behandelt. Der erste Teil der Arbeit besteht aus zwei Unterteilen. Im ersten Unterteil werden separable Kanäle (SEP) betrachtet, d.h., Kanäle, die mittels separabler Krausoperatoren dargestellt werden können. SEP bildet eine strikte übermenge der Menge der Quantenoperationen, die mittels lokaler Operationen und klassischer Kommunikation implementiert werden können (LOCC). Dabei ist LOCC genau die Menge von Quantenoperationen, mittels welcher keine Verschränkung erzeugt werden kann. Separable Transformationen erlauben es notwendige Bedingung für LOCC-Transformationen herzuleiten. Wir zeigen, dass es nicht hinreichend ist nur Kanäle zu betrachten, die mittels separabler und invertierbarer Krausoperatoren dargestellt werden können (SEP1), um zu entscheiden ob zwei reine Zustände mit SEP ineinander transformiert werden können. Dieses Resultat wirft die Frage auf, ob Transformationen mittels SEP1 notwendig sind für LOCC-Transformationen. Während die Relation von SEP1 und LOCC nicht abschließend geklärt werden konnte, wird im Folgenden gezeigt, dass SEP1-Transformationen notwendig sind für Transformationen mittels LOCC-Protokollen, die nur aus endlich vielen Runden klassischer Kommunikation bestehen (LOCCN), also solche LOCC-Protokolle, die physikalisch relevant sind. Darüber hinaus werden notwendige und hinreichende Bedingungen dafür hergeleitet, wann eine Transformation zwischen zwei reinen Zuständen mittels SEP möglich ist (siehe auch [Gour et al. New Journal of Physics 13(7), 073013 (2011)]). Im zweiten Unterteil wird die Verschränkung von Stabilizerzuständen untersucht, da diese Zustände viele Anwendungen in der Quanteninformationstheorie besitzen. Dazu werden lokale Transformationen dieser Zustände betrachtet. Als Voraussetzung dafür werden zunächst alle lokalen Symmetrien von Stabilizerzuständen charakterisiert. Zudem wird ein Algorithmus hergeleitet, um diese für einen gegebenen Zustand zu bestimmen. Diese Ergebnisse werden dann verwendet um LOCCN-Transformatio- nen innerhalb der äquivalenzklasse zu analysieren, die von einem Stabilizerzustand und allen Zuständen, die unter probabilistischen LOCC-Transformationen von diesem erreicht werden können, gebildet wird (SLOCC). Zudem werden Anwendungen von Stabilizerzuständen diskutiert, die aus den Eigenschaften ihrer lokalen Symmetriegruppe abgeleitet werden können. Um einen vergröberten Blick auf die Verschränkung von Stabilizerzuständen zu erhalten, werden dann Cliffordtransformationen zwischen diesen Zuständen untersucht, die lokal bezüglich einer fixierten Menge von Parteien wirken (PLC). Eine solche Partei kann dabei aus mehr als einem Qubit bestehen. Zunächst wird gezeigt, dass PLC Transformationen zwischen Graphenzuständen durch eine verallgemeinerte Form von lokaler Komplementierung beschrieben werden kann. Letztere beschreibt Transformationen zwischen Graphenzuständen mittels lokaler Cliffordoperatoren. Um die entstehenden Äquivalenzklassen zu charakterisieren wird die so genannte verschränkung-generierende Menge (EGS) verwendet [Bravyi et al., J. Math. Phys. 47, 062106 (2006)]. Diese Menge enthält für bis zu drei Parteien nur endlich viele Zustände [Bravyi et al., J. Math. Phys. 47, 062106 (2006)]. Im Folgenden wird gezeigt, dass das EGS für vier und mehr Parteien unendlich viele Elemente enthält. Im zweiten Teil der Arbeit wird die partielle Unterscheidbarkeit von identischen Teilchen in Interferenzexperimenten untersucht, in welchen einige Freiheitsgrade der Teilchen nicht verändert und nicht detektiert werden. Dabei werden insbesondere Bosonen betrachtet. Anwendungen solcher Interferenzexperimente benötigen meist ununterscheidbare Teilchen. Deshalb spielt die Charakterisierung von partieller Unterscheidbarkeit sowie deren Quantifizierung eine wichtige Rolle. Zunächst wird in diesem Teil der Arbeit Literatur zusammengefasst, die für die weiteren Kapitel besonders relevant ist. Diese Literatur beschäftigt sich hauptsächlich mit bestimmten Teilmengen von Zuständen, die relevant sind für Experimente. Ausgehend von dieser Zusammenfassung wird dann eine Definition von Ununterscheidbarkeit und Unterscheidbarkeit für Teilchen formuliert, die durch allgemeine Zustände beschrieben werden. Diese basiert alleinig auf den Informationen über die Teilchen, welche auch in den betrachteten Experimenten zugänglich sind. Die zugehörigen Mengen von Zuständen werden mittels Darstellungstheorie charakterisiert. Darüber hinaus wird eine effiziente Methode hergeleitet um eine obere und eine untere Schranke an ein Ununterscheidbarkeitsmaß mittels Interferenzexperimenten zu bestimmen, welches sich von der Definition von Ununterscheidbarkeit ableitet.