Privacy preserving authenticated Kkey exchange : Modelling, constructions, proofs and formal verification : Modellierung, Konstruktionen, Beweise und Verification

Abstract

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.

Privacy preserving authenticated key exchange (PPAKE) protocols are authenticated key exchange (AKE) protocols that aim to hide the identities of the communicating parties from third parties. Hence the security models of AKE are extended with additional properties. PPAKE protocols have been studied previously. Our aim is to strengthen the existing privacy properties of such protocols. Most notably we additionally consider attacks in which the adversary does not complete the protocol run (e.g. due to the inability to authenticate itself). These attacks are relevant because since some adversaries might not even care if the protocol run is aborted after they deanonymize their target. Furthermore we introduce a formal model that incorporates these properties and several protocols that fulfill different levels of privacy. One of the protocols is a generic construction from generic cryptographic building blocks and hence allows for a post-quantum secure instantiation. Additonally we present formal proofs of all protocols in our model. The second part of this thesis deals with the automated verification of the privacy properties of the main protocol of the first part. Automated verification is used to either find an attack or conclude that the specified properties indeed hold. This gives additional confidence in the correctness of the security proofs contained in this work. First we evaluated the protocol using the Tamarin Prover, which however is unable to finish its proof or find a contradiction with the given resources (approx. 60 GB memory). Then we utilized the verification software ProVerif and were able to prove the security of the protocol. We will present both the Tamarin Prover encoding as well as the ProVerif encoding.