Analysis of selected cryptographic protocols with DY*

Abstract

DY* is a framework implemented in the proof-oriented programming language F*, aiming at symbolic analysis of cryptographic protocols on the structural and on the implementation level. In this master's thesis, we analyse three selected authentication and key exchange protocols with DY*: the Otway-Rees protocol, the Yahalom protocol and the Denning-Sacco protocol with public keys. Each of these protocols is designed to establish a secure channel between two users while involving a trusted third party in the authentication process. The Otway-Rees and Yahalom protocols rely on pre-shared symmetric keys with this trusted third party, while the Denning-Sacco protocol relies on digital signatures and public key encryption. In addition, the Denning-Sacco protocol proposes the use of timestamps in messages to provide users with guarantees about the timeliness of the conversation, a protocol feature that has not yet been attempted to be modeled and analyzed in DY*. We developed accurate models for each of the three protocols in DY*, documented possible attacks and proposed improvements to prevent them, and finally proved the security of the protocol or its improved version. We found several attacks on the Otway-Rees protocol that allow an adversary to impersonate one or possibly both of the users involved in the protocol, and based on these attacks, presented improvements to prevent them. For the Yahalom protocol, we show that it satisfies security goals derived from its formal specification, and draw parallels to other approaches with similar results. We also comment on the differences between our results and those of other analyses that describe the Yahalom protocol as flawed. Moreover, we developed an extension to DY* for modeling time-based properties of protocols with timestamps and demonstrated it on the Denning-Sacco protocol. As a result, we provide the first symbolic security proof, including timestamp-dependent security properties, of the Denning-Sacco protocol in DY*.

DY* ist ein in der beweisorientierten Programmiersprache F* implementiertes Framework zur symbolischen Analyse von kryptographischen Protokollen auf der Struktur- und Implementierungsebene. In dieser Masterarbeit analysieren wir drei ausgewählte Authentifizierungs- und Schlüsselaustauschprotokolle mit DY*: das Otway-Rees Protokoll, das Yahalom Protokoll und das Denning-Sacco Protokoll mit öffentlichen Schlüsseln. Jedes dieser Protokolle ist darauf ausgelegt, einen sicheren Kanal zwischen zwei Benutzern aufzubauen und dabei eine vertrauenswürdige dritte Partei in den Authentifizierungsprozess einzubeziehen. Die Protokolle Otway-Rees und Yahalom beruhen auf gemeinsam genutzten symmetrischen Schlüsseln mit dieser vertrauenswürdigen dritten Partei, während das Denning-Sacco Protokoll auf digitalen Signaturen und Verschlüsselung mit öffentlichen Schlüsseln beruht. Darüber hinaus schlägt das Denning-Sacco Protokoll die Verwendung von Zeitstempeln in Nachrichten vor, um den Benutzern Garantien in Bezug auf die Aktualität der Konversation zu geben - eine Protokolleigenschaft, die in DY* noch nicht modelliert und analysiert wurde. Wir haben präzise Modelle für jedes der drei Protokolle in DY* entwickelt, mögliche Angriffe dokumentiert und Verbesserungen vorgeschlagen, um sie zu verhindern, und schließlich die Sicherheit des Protokolls oder seiner verbesserten Version bewiesen. Wir konnten mehrere Angriffe auf das Otway-Rees Protokoll finden, die es einem Angreifer ermöglichen, sich als einer oder möglicherweise als beide am Protokoll beteiligten Benutzer auszugeben, und haben auf der Grundlage dieser Angriffe Verbesserungen zur Verhinderung derselben vorgestellt. Für das Yahalom Protokoll zeigen wir, dass es die aus seiner formalen Spezifikation abgeleiteten Sicherheitsziele erfüllt, und ziehen Parallelen zu anderen Ansätzen mit ähnlichen Ergebnissen. Wir kommentieren auch die Unterschiede zwischen unseren Ergebnissen und denen anderer Analysen, die das Yahalom Protokoll als unsicher bezeichnen. Darüber hinaus haben wir eine Erweiterung von DY* für die Modellierung zeitbasierter Eigenschaften von Protokollen mit Zeitstempeln entwickelt und diese am Denning-Sacco Protokoll demonstriert. Als Ergebnis liefern wir den ersten symbolischen Sicherheitsbeweis, einschließlich von Zeitstempeln abhängiger Sicherheitseigenschaften, für das Denning-Sacco Protokoll in DY*.