Formal Security Analysis of Widevine through the W3C EME Standard

Streaming services such as Netflix, Amazon Prime Video, or Disney+ rely on the widespread EME standard to deliver their content to end users on all major web browsers. While providing an abstraction layer to the underlying DRM protocols of each device, the security of this API has never been formally studied. In this paper, we provide the first formal analysis of Widevine, the most deployed DRM instantiating EME.

We define security goals for EME, focusing on media protection and usage control. Then, relying on the TAMARIN prover, we conduct a detailed security analysis of these goals on some Widevine EME implementations, reverse-engineered by us for this study. Our investigation highlights a vulnerability that could allow for unlimited media consumption. Additionally, we present a patched protocol that is suitable for both mobile and desktop platforms, and that we formally proved secure using TAMARIN. lemma CDMKeysInit[reuse, use_induction]: "∀ #i rID sID kAsset kMacS kMacC. Keys(rID, sID, kAsset, kMacS, kMacC)@#i ⇒ ( (∃ #j. (#j < #i) & Derive(rID, sID, kAsset, kMacS, kMacC)@#j) | (kAsset ='null' & kMacS = 'null' & kMacC = 'null'))"