OpenID for Verifiable Credentials : formal security analysis using the Web Infrastructure Model

Abstract

In our increasingly connected world, digital identities play a fundamental role in delivering secure online services around the globe. To enable the seamless exchange of identification data among various entities, the adoption of standardized protocols is essential. The protocol family OpenID for Verifiable Credentials (OID4VC) is ideally suited for exchanging identities. The two most important protocols in this family are OpenID for Verifiable Credential Issuance (OID4VCI) and OpenID for Verifiable Presentations (OID4VP) with a wide range of applications in e-government as well as in the private sector. A prominent example is the European Digital Identity Framework, which includes these two protocols, among others. This means that any future wallet in the European Union will implement OID4VCI and OID4VP. Therefore, it is extremely important to guarantee their security. This thesis performs a rigorous formal security analysis of both the OpenID for Verifiable Credential Issuance and the OpenID for Verifiable Presentations protocols. In particular, we focus on analyzing the security of both protocols when they interact in an ecosystem. It is not sufficient to consider the two protocols separately, because the interaction between them may introduce new vulnerabilities. Therefore, the formal model created in this thesis models both protocols simultaneously. The model is based on the Web Infrastructure Model (WIM), which closely follows existing web technologies. To describe what security means in this context, we define an authentication security property and a session integrity security property for OID4VCI and OID4VP. We prove that the model is secure with respect to the security properties under the assumption of a vigilant user. If this assumption is violated, we have discovered a number of attacks. This work makes several contributions to the protocol specifications: First, the discovered vulnera- bilities were brought to the attention of the working group. Second, several issues were filed to improve the quality and security of the specifications. Lastly, we engaged in ongoing discussions on related issues.

In unserer immer stärker vernetzten Welt spielen digitale Identitäten eine fundamentale Rolle bei der Bereitstellung von sicheren Online-Dienstleistungen auf der ganzen Welt. Um den nahtlosen Austausch von Identitätsdaten zwischen verschiedenen Organisationen zu ermöglichen, ist die Einführung von standardisierten Protokollen unerlässlich. Die Protokollfamilie OpenID for Verifiable Credentials (OID4VC) ist ideal geeignet für den Austausch von Identitäten. Die beiden wichtigsten Protokolle der Familie sind OpenID for Verifiable Credential Issuance (OID4VCI) und OpenID for Verifiable Presentations (OID4VP). Diese haben ein breites Anwendungsspektrum sowohl bei E-Government Services als auch in der Privatwirtschaft. Ein prominentes Beispiel ist das European Digital Identity Framework, das unter anderem die beiden Protokolle OID4VCI und OID4VP beinhaltet. Das bedeutet, dass jedes zukünftige Wallet in der Europäischen Union diese Protokolle implementieren wird. Daher ist es äußerst wichtig, ihre Sicherheit zu gewährleisten. In dieser Arbeit wird eine gründliche formale Sicherheitsanalyse der Protokolle OpenID for Verifiable Credential Issuance und OpenID for Verifiable Presentations durchgeführt. Insbesondere konzentrieren wir uns auf die Analyse der Sicherheit beider Protokolle, wenn sie in einem Ökosystem interagieren. Es reicht nicht aus, die beiden Protokolle getrennt zu betrachten, da die Interaktion zwischen ihnen neue Schwachstellen hervorbringen kann. Daher modelliert das in dieser Arbeit erstellte formale Modell beide Protokolle gleichzeitig. Das Modell basiert auf dem Web Infrastructure Model (WIM), das sich eng an bestehenden Webtechnologien orientiert. Um zu beschreiben, was Sicherheit in diesem Zusammenhang bedeutet, definieren wir die beiden Sicherheitseigenschaften Authentication und Session Integrity für OID4VCI und OID4VP. Dann zeigen wir, dass das Model in Bezug auf diese Sicherheitseigenschaften unter der Annahme eines aufmerksamen Benutzers sicher ist. Für den Fall, dass diese Annahme verletzt wird, haben wir eine Reihe von Angriffen entdeckt. Diese Arbeit liefert mehrere Beiträge zu den Protokollspezifikationen. Erstens wurden die entdeckten Schwachstellen der Arbeitsgruppe zur Kenntnis gebracht. Zweitens wurden mehrere Issues zur Verbesserung der Qualität und Sicherheit der Spezifikationen eingereicht. Zudem haben wir aktiv an den laufenden Diskussionen zu den Themen teilgenommen.