Was kryptografische Protokolle angeht, ist ein formaler Sicherheitsbeweis das Qualitätsmerkmal erster Güte. Deutsche Forscher liefern nun einen solchen Beweis für das Ibex-Protokoll und bestätigen damit, dass Threemas Sicherheit auf grundsolidem Fundament beruht.
Vor ein paar Monaten haben wir «Ibex» lanciert. Das neue kryptografische Kommunikationsprotokoll hat Threemas bewährte Sicherheit weiter gefestigt, Perfect Forward Secrecy auf Ende-zu-Ende-Ebene eingeführt und das Gesamtsystem für die Zukunft gerüstet.
Drei ausgewiesene Sicherheitsforscher des Lehrstuhls für Angewandte Kryptografie der Friedrich-Alexander-Universität Erlangen-Nürnberg legen nun eine eingehende Sicherheitsanalyse des Protokolls vor. Mit einem formalen Beweis bestätigen sie die Sicherheit von Ibex und unterstreichen dessen kryptografische Robustheit:
Durch eine umfassende Untersuchung haben wir die Einhaltung der versprochenen Sicherheitseigenschaften des Protokolls erfolgreich evaluiert. Die Ergebnisse unserer Analyse zeigen, dass das Ibex-Protokoll die gewünschten Sicherheitsanforderungen zufriedenstellend erfüllt. Insbesondere wurden bei unserer Untersuchung keine Fehler oder Schwachstellen im Protokoll gefunden. Dass Ibex einer strengen Sicherheitsanalyse standgehalten hat und wir in der Lage waren, die Sicherheit des Protokolls formal zu beweisen, ist Beleg für dessen solides kryptografisches Design. Die Absenz nennenswerter Schwachstellen stärkt das Vertrauen in die Sicherheitsgarantien des Protokolls weiter und erhöht seine allgemeine Vertrauenswürdigkeit. (S. 36)
Um die Sicherheit von Ibex nachzuweisen, wenden die Forscher modernste Verfahrensweisen an und führen einen Widerspruchsbeweis. Sie zeigen auf, dass die Annahme, ein Angreifer könne Threema-Nachrichten mitlesen, bedingen würde, dass er das Gap-Diffie-Hellman-Problem in polynomieller Zeit löst. Weil jedoch davon ausgegangen wird, dass kein effizienter Angreifer dazu in der Lage ist, kann auch kein Angreifer Threema-Nachrichten lesen. Somit verfügt Ibex über beweisbare Sicherheit, und Vertraulichkeit ist garantiert. Das Forschungsteam demonstriert ausserdem, dass neben Vertraulichkeit weitere Sicherheitsgarantien gegeben sind, insb. Integrität, Authentizität und Perfect Forward Secrecy.
In Anbetracht dieses positiven Ergebnisses ist Perfect Forward Secrecy in den heute erschienenen Mobil-Apps (Threema 5.1 für Android und Threema 5.4 für iOS) standardmässig aktiviert.
Wir bedanken uns bestens bei Prof. Dominique Schröder, Prof. Paul Rösler und Paul Gerhart für die akribische Arbeit und ihr ausserordentliches Engagement. Um die vollständige Sicherheitsanalyse (auf Englisch) zu lesen, folgen Sie bitte diesem Link: