The rapid and promising development of applications and communication systems designed for groups of participants like groupware, computer supported collaborative work systems, or digital conference systems implies exigence of mechanisms providing adequate security properties. These mechanisms can be designed based on the foundations of cryptography. Group key exchange protocols are multi-party cryptographic protocols those participants compute a shared secret key that can then be used in conjunction with other cryptographic constructions like encryption schemes and message authentication codes for the purpose of privacy, confidentiality and authentication. Security confidence of modern cryptographic constructions can be increased via adequate security proofs. The paradigm of provable security gains in importance for all kinds of cryptographic constructions, including group key exchange protocols those security issues represent the scope of this dissertation. We give an analytical overview of the state-of-the-art research in this area and identify strengths and weaknesses of many previous approaches. We suggest a new approach in form of a security model those stronger definitions provide background for more confident security analyzes and proofs. Additionally, we present a number of generic solutions (compilers) that can be applied to independently designed group key exchange protocols in order to enhance security thereof with respect to various goals considered by our security model. Finally, we present a concrete group key exchange protocol that provably satisfies the apparently strongest currently available formally specified security requirements. Abstract (in German)in German) Die schnelle und vielversprechende Entwicklung der fur Gruppen von Teilnehmern konzipierten Anwendungen und Kommunikationssysteme, wie z.B. Groupware, Systeme fur die computergestutzte Gruppenarbeit oder digitale Konferenzsysteme, schafft die Notwendigkeit von Mechanismen zur Gewahrleistung ausreichender Sicherheitseigenschaften. Der Entwurf dieser Mechanismen basiert grostenteils auf den Grundlagen der Kryptografie. Gruppen-SchlusselAustauschprotokolle (engl. group key exchange protocols) sind kryptografische MehrparteienProtokolle, die es den Teilnehmern ermoglichen, sich auf einen gemeinsamen geheimen Schlussel zu einigen, der in Verbindung mit weiteren kryptografischen Verfahren, wie z.B. Verschlusselungsund Nachrichtenauthentisierungsverfahren, fur die Geheimhaltung, Vertraulichkeit und Authentisierung eingesetzt werden kann. Das Vertrauen in die Sicherheit der modernen kryptografischen Verfahren kann heutzutage nur mittels eines ausreichenden Sicherheitsbeweises erzielt werden. Das Paradigma der beweisbaren Sicherheit gewinnt immer mehr an Bedeutung fur alle kryptografischen Verfahren, einschlieslich der Gruppen-Schlussel-Austauschprotokollen, deren Sicherheitsaspekte den Hauptbestandteil dieser Dissertation darstellen. Wir geben einen analytischen Uberblick uber den aktuellen Stand der Forschung in diesem Bereich und heben Starken und Schwachen vieler bekannter Ansatze hervor. Ausgehend von den durchgefuhrten Analysen und gefundenen Mangeln der vorhandenen Ansatze und Verfahren schlagen wir einen neuen Ansatz vor, in Form eines Sicherheitsmodells fur Gruppen-SchlusselAustauschprotokolle, das weitaus starkere Sicherheitsanforderungen umfasst und die Basis fur tiefere Sicherheitsanalysen und Beweise bereit stellt. Zusatzlich, stellen wir eine Reihe von allgemeinen Losungen zur Verbesserung der Sicherheit (im Rahmen unseres Modells) von unabhangig konzipierten Gruppen-Schlussel-Austauschprotokollen vor. Abschliesend beschreiben wir ein neues Gruppen-Schlussel-Austauschprotokoll, dessen beweisbare Sicherheit den derzeit starksten formalen Anforderungen entspricht.
The rapid and promising development of applications and communication systems designed for groups of participants like groupware, computer supported collaborative work systems, or digital conference systems implies exigence of mechanisms providing adequate security properties. These mechanisms can be designed based on the foundations of cryptography. Group key exchange protocols are multi-party cryptographic protocols those participants compute a shared secret key that can then be used in conjunction with other cryptographic constructions like encryption schemes and message authentication codes for the purpose of privacy, confidentiality and authentication. Security confidence of modern cryptographic constructions can be increased via adequate security proofs. The paradigm of provable security gains in importance for all kinds of cryptographic constructions, including group key exchange protocols those security issues represent the scope of this dissertation. We give an analytical overview of the state-of-the-art research in this area and identify strengths and weaknesses of many previous approaches. We suggest a new approach in form of a security model those stronger definitions provide background for more confident security analyzes and proofs. Additionally, we present a number of generic solutions (compilers) that can be applied to independently designed group key exchange protocols in order to enhance security thereof with respect to various goals considered by our security model. Finally, we present a concrete group key exchange protocol that provably satisfies the apparently strongest currently available formally specified security requirements. Abstract (in German)in German) Die schnelle und vielversprechende Entwicklung der fur Gruppen von Teilnehmern konzipierten Anwendungen und Kommunikationssysteme, wie z.B. Groupware, Systeme fur die computergestutzte Gruppenarbeit oder digitale Konferenzsysteme, schafft die Notwendigkeit von Mechanismen zur Gewahrleistung ausreichender Sicherheitseigenschaften. Der Entwurf dieser Mechanismen basiert grostenteils auf den Grundlagen der Kryptografie. Gruppen-SchlusselAustauschprotokolle (engl. group key exchange protocols) sind kryptografische MehrparteienProtokolle, die es den Teilnehmern ermoglichen, sich auf einen gemeinsamen geheimen Schlussel zu einigen, der in Verbindung mit weiteren kryptografischen Verfahren, wie z.B. Verschlusselungsund Nachrichtenauthentisierungsverfahren, fur die Geheimhaltung, Vertraulichkeit und Authentisierung eingesetzt werden kann. Das Vertrauen in die Sicherheit der modernen kryptografischen Verfahren kann heutzutage nur mittels eines ausreichenden Sicherheitsbeweises erzielt werden. Das Paradigma der beweisbaren Sicherheit gewinnt immer mehr an Bedeutung fur alle kryptografischen Verfahren, einschlieslich der Gruppen-Schlussel-Austauschprotokollen, deren Sicherheitsaspekte den Hauptbestandteil dieser Dissertation darstellen. Wir geben einen analytischen Uberblick uber den aktuellen Stand der Forschung in diesem Bereich und heben Starken und Schwachen vieler bekannter Ansatze hervor. Ausgehend von den durchgefuhrten Analysen und gefundenen Mangeln der vorhandenen Ansatze und Verfahren schlagen wir einen neuen Ansatz vor, in Form eines Sicherheitsmodells fur Gruppen-SchlusselAustauschprotokolle, das weitaus starkere Sicherheitsanforderungen umfasst und die Basis fur tiefere Sicherheitsanalysen und Beweise bereit stellt. Zusatzlich, stellen wir eine Reihe von allgemeinen Losungen zur Verbesserung der Sicherheit (im Rahmen unseres Modells) von unabhangig konzipierten Gruppen-Schlussel-Austauschprotokollen vor. Abschliesend beschreiben wir ein neues Gruppen-Schlussel-Austauschprotokoll, dessen beweisbare Sicherheit den derzeit starksten formalen Anforderungen entspricht.
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.
Authenticated key-exchange protocols allow two participants A and B , communicating over a public network and each holding an authentication means to exchange a shared secret value. Methods designed to deal with this cryptographic problem ensure A (resp. B ) that no other participants aside from B (resp. A ) can learn any information about the agreed value and often also ensure A and B that their respective partner has actually computed this value. A natural extension to this cryptographic method is to consider a pool of participants exchanging a shared secret value and to provide a formal treatment for it. Starting from the famous two-party Diffie--Hellman (DH) key-exchange protocol and from its authenticated variants, security experts have extended it to the multiparty setting for over a decade and, in the past few years, completed a formal analysis in the framework of modern cryptography. The present paper synthesizes this body of work on the provably-secure authenticated group DH key exchange.
In der vorliegenden Arbeit behandeln wir verschiedene Themen aus dem Gebiet der Quanteninformationstheorie. Die unterschiedlichen Ergebnisse sollen entweder die Anwendung theoretischer Konzepte auf reale Experimente erleichtern oder bei der weiterfuhrenden Arbeit an zentralen Fragen helfen. Im Detail werden folgende Punkte untersucht: Wir wenden uns als Erstes der Fragestellung zu, unter welchen Vorraussetzungen eine gegebene Menge an Erwartungswerten mit den ersten beiden Momenten der Spinoperatoren eines Zustandes von Gesamtspin j kompatible ist. Hierbei liegt das Hauptaugenmerk auf einer operationellen Beschreibung, so dass man direkt mit den Momenten arbeiten kann, anstatt den kompletten Dichteoperator zu verwenden. Wir zeigen, dass diese Charakterisierung physikalischer Momente zu dem Problem der Bose-symmetrischen Erweiterungen fur speziell bestimmte Zweiqubit Zustande aquivalent ist. Mittels dieser Umformulierung bestimmen wir operationelle Teil- und Ubermengen der exakten Menge, um somit auf einfache Art und Weise Momente identifizieren zu konnen, die sicher physikalisch sind, als auch andere, die eindeutig inkompatibel mit den Vorhersagen der Quantenmechanik sind. Diese approximative Losung gewinnt mit steigender Gesamtspinzahl j an Genauigkeit, und konvergiert im Limes gegen die exakte Losung. Im nachsten Abschnitt beschaftigen wir uns mit dem Konzept der Verschrankungszeugen; der gebrauchlichsten Methode zur Verschrankungsdetektion. Wir untersuchen, wie man die Qualitat eines linearen Verschrankungszeugen durch quadratische, nichtlineare Terme verbessen kann, so dass man mehr verschrankte Zustande auf einmal detektiert. Das betrachtete Verbessungsschema hat den Vorteil dass man es iterative benutzen kann. Dies liefert eine Abfolge von Verschrankungszeugen mit Nichtlinearitaten immer hoherer Ordnung, deren Starke in jedem Schritt zunimmt. Die entwickelte Iterationsmethode kann fur verschiedene Aufgaben verwendet werden und wir betrachten zwei ausgezeichnete Extremfalle: Entweder optimieren wir fur einen vorgegeben Zielzustand oder fur alle moglichen Zustande gleichmassig. Im restlichen Teil der Arbeit untersuchen wir verschiedene Moglichkeiten, wie man bereits vorhandene Ideen besser an reale Experimente anpasst. Hier sei angemerkt dass viele Anwendungen der Quanteninformationstheorie nur fur stark idealisierte Systeme vorgeschlagen und diskutiert wurden und somit nicht direkt fur das Experiment anwendbar sind. Dieser Punkt ist fur das Feld der Quantenschlusselverteilung von besonderer Bedeutung, da man die vorbehaltslose Sicherheit eines realen, durch ein Experiment generierten Schlussels zeigen mochte und nicht nur fur die einer idealisierten Version davon. Mit diesem Ziel im Hinterkopf untersuchen wir zuerst die theoretische Idee des Squash Modells. Dieses bietet einen eleganten Ausrechentrick', der es erlaubt, die Sicherheitsanalyse eines idealisierten Quantenschlusselverteilungsprotokolls direkt fur das reale Experiment zu verwenden. Wir entwickeln einen Formalismus zur Prufung dieses Squash Modells fur einen gegebenen Messaufbau und betrachten relevante Messschemen mit und ohne dieser Eigenschaft. Im Gegensatz zu diesem theoretischen Modell behandlen wir auch eine experimentelle Moglichkeit, die es uns erlaubt, die Sicherheitsanalyse des idealisierten Systems direkt fur das reale Experiment zu verwenden. Dazu benutzen wir die Idee, dass man durch die Kombination eines variablen Strahlteilers mit einem einfachen Click/No-Click' Detektor, die Statistik von photonauflosenden Detektoren erhalten kann. Durch diese Hardwareanderung ist es moglich, die sicherheitsrelevanten Parameter direkt abzuschatzen. Diese Methode bietet somit auch einen Weg, die Sicherheit eines realen Quantenschlusselverteilungsexperiments zu beweisen, fur das die theoretische Squash Modell Idee nicht funktioniert. Als Ergebnis erhalt man unter anderem einen neuen Distanzrekord fur ein reales Quantenschlusselverteilungsexperiment mit derzeitiger Technologie. Als letzten Punkt betrachten wir das Problem der experimentellen Verschrankungsverifizierung. Bei dieser Verifizierung hat man oftmals ein Praktikabilitatsproblem, weil man---ob verschiedener Grunde---meistens nur ein sehr vereinfachtes Modell fur die verwendenten Messapparate benutzt. Wir zeigen, dass man in diesem Fall der Fehlinterpretation der beobachteten Messausgange durchaus Fehler machen kann, allerdings untersuchen wir in erster Linie Bedingungen, unter denen ein falschlicher Verschrankungsnachweis ausgeschlossen werden kann. Zu diesem Zweck verwenden wir ein dem Squash Modell ahnliches, aber weniger restriktives Konzept. Eine interessante Anwendung liefern die ublicherweise mittels Tomographie durchgefuhrten Verschrankungstests, die man typischerweise fur parametrische Fluoreszenz Quellen oder fur photonische Mehrparteienexperimente verwendet. Wir zeigen, dass diese sehr einfach fehlerfrei gemacht werden konnen.
Group key exchange protocols allow their participants to compute a secret key which can be used to ensure security and privacy for various multi- party applications. The resulting group key should be computed through coop- eration of all protocol participants such that none of them is trusted to have any advantage concerning the protocol's output. This trust relationship states the main difference between group key exchange and group key transport protocols. Obvi- ously, misbehaving participants in group key exchange protocols may try to influ- ence the resulting group key, thereby disrupting this trust relationship, and also causing further security threats. This paper analyzes the currently known secu- rity models for group key exchange protocols with respect to this kind of attacks by malicious participants and proposes an extended model to remove the identi- fied limitations. Additionally, it proposes an efficient and provably secure generic solution, a compiler, to guarantee these additional security goals for group keys exchanged in the presence of malicious participants.
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.
Das Ziel der Quantenschlusselverteilung ist die Erstellung eines sicheren Schlussels, verteilt zwischen zwei Parteien Alice und Bob, die durch einen Quantenkanal und einen authentifizierten klassischen Kanal verbunden sind. Fur gewohnlich wurden sichere Schlusselraten hauptsachlich in dem unrealistischen Fall von unendlich vielen Signalen berechnet. Erst kurzlich wurden Szenarien der Quantenschlusselverteilung analysiert, die eine finite Anzahl an durch den Kanal versendeten Signalen betrachten und den Lauscher nicht auf eine spezifische Attacke einschranken. Die Herausforderung dieser Doktorarbeit ist es, Strategien zur Optimierung geheimer Schlusselraten fur die finite Quantenschlusselverteilung zu entwickeln. Wir prasentieren zwei Arten von Optimierungsmethoden.
Zunachst modifizieren wir das Protokoll, indem wir einen vorbehandelnden Schritt hinzufugen, der nutzliche Effekte auf die sichere Schlusselrate haben kann. Genauer gesagt untersuchen wir den Effekt unterschiedlicher Rauschszenarien auf die erreichbare Rate eines epsilon-sicheren Schlussels fur das BB84- und 6-Zustand-Protokoll unter der Annahme von kollektiven Attacken. Wir zeigen, dass, auf der einen Seite absichtliches Hinzufugen von Rauschen zu einer Erhohung der sicheren Schlusselrate fuhren kann, und auf der anderen Seite erhoht sich die geheime Schlusselrate deutlich unter der realistischen Annahme, dass ein realer Kanal Rauschen erzeugt, das nicht einem Lauscher zugesprochen werden muss.
Die zweite Vorgehensweise beinhaltet die Optimierung der mathematischen Sicherheitsanalyse. Unterschiedliche Arten von Entropien spielen bei der Analyse von finiter Quantenschlusselverteilung eine Rolle. Zum Beispiel konnen die glatte Min-Entropie und die Renyi-Entropien zur Berechnung sicherer Schlusselraten fur finite Quantenschlusselverteilung verwendet werden. Da diese Entropien aber fur hochdimensionale Systeme sehr schwierig oder sogar unmoglich zu berechnen sind, werden berechenbare Abschatzungen fur diese Entropien sehr wichtig. Neben der fur Tensorproduktzustande hergeleiteten von-Neumann-Entropie-Abschatzung, die fur experimentell zugangliche Situationen pessimistische geheime Schlusselraten liefert, und neben einer sehr spezifischen Verfahrensweise fur das BB84-Protokoll, sind keine weiteren Abschatzungen bekannt. Diese Lucke wird durch diese Doktorarbeit geschlossen: Wir berechnen eine erreichbare geheime Schlusselrate fur die Quantenschlusselverteilung mit finiter Anzahl an Signalen, indem wir die glatte Min-Entropie durch die Min-Entropie eines Einzelkopiezustands abschatzen. Durch explizite Auswertung der Min-Entropie unter der Verwendung ihrer Verbindung zur Ratewahrscheinlichkeit finden wir nichtverschwindende Schlusselraten schon fur weniger Signale als im Vergleich zum von-Neumann-Entropie-Ansatz. Eine weitere Abschatzung an die sichere Schlusselrate wird hergeleitet, die sich als Optimierungsproblem uber Renyi-Entropien darstellt. Unter der Annahme von kollektiven Attacken entwickeln wir eine berechenbare Abschatzung fur das 6-Zustand-Protokoll, die zu verbesserten geheimen Schlusselraten im Vergleich zu vorhergehenden Resultaten fuhrt.
Zusatzlich entwickeln wir eine neue Methode, geheime Schlusselraten fur pemutationsinvariante Protokolle fur koharente Attacken und finite Ressourcen zu quantifizieren. Durch einen Vergleich der Resultate mit der bekannten Post-selection-Technik fur das BB84- und 6-Zustand-Protokoll wird die hohe Relevanz dieser Methode deutlich. Da die Einschrankung auf die Klasse der permutationsinvarianten Protokolle recht schwach ist, hebt dies die breite Wichtigkeit dieser Resultate hervor. Zusatzlich zu der Bestatigung der bekannten Aquivalenz zwischen koharenten und kollektiven Attacken fur permutationsinvariante Protokolle im Grenzfall unendlich vieler Quantensignale, geben die Resultate dieser Arbeit moglicherweise Hinweise darauf, dass diese Aquivalenz fur den Fall finiter Ressourcen nicht mehr gewahrleistet ist.