Provable Non-Frameability for 5G Lawful Interception

Abstract

Mobile networks have grown in size and relevance, with novel applications in areas including transportation, finance, and health. The wide use of mobile networks generates rich data about users, raising interest in using such data for law enforcement and antiterrorism through Lawful Interception (LI). Countries worldwide have established legal frameworks to conduct LI, and technical standards have been created for its implementation and deployment, but without sufficient (and rigorous) security controls. While LI originated for benign purposes, we show in this paper that malicious entities could exploit it to frame users into suspicion of criminal activity. Further, we propose a solution for non-frameability, which we formally prove uphold desired properties even in scenarios where attackers completely infiltrate the operator networks. To perform the formal verification, we extend prior work with a more complete model of the fifth generation (5G) of mobile networks in the Tamarin prover.