Authentic Communication and Trustworthy Location in Mobile Networks

Widespread mobile network connectivity has changed society and, consequently, increased our dependency on its proper functioning for transportation, safety, finance, and more. This thesis is concerned with improving the security of mobile networks and focuses on two such instances: vehicular and cellular networks. We aim at mitigating certain security risks even in the presence of strong attackers, which could be manifested in the form of internal malicious agents in cellular network providers or connected vehicles compromised with malicious software, to mention a couple of examples. Within this scope, we target two main challenges: proving that a selected set of security protocols in vehicular and cellular networks guarantee the expected security properties and improving the trustworthiness of location information shared by neighbouring vehicles. Our contributions to security protocols involve employing formal methods to verify security properties in the vehicular communication protocol Ensemble and in the fifth generation of cellular networks (5G). The Ensemble protocol aims to enable multi-brand truck platooning and is currently in a prestandardisation effort in Europe. We report a potential weakness that was resolved in the latest versions and verify that strong security properties are fulfilled. To make verification tractable, we propose a strategy based on the hierarchy of cryptographic keys which may also be employed in protocols that have similar keying structures. In 5G, we identify a weakness that could be exploited to frame people into suspicion of serious crimes when lawful interception operations are conducted. We then design the changes required to guarantee non-frameability in 5G and formally verify the expected security properties. In the context of location trustworthiness, we design and evaluate a proof-of-location scheme tailored for vehicular networks called Vouch+. Vouch+ can operate in centralised or decentralised modes and combines location information shared by neighbouring vehicles (or the infrastructure) with a plausibility model to ensure the validity of the position claimed by other vehicles. Furthermore, we propose and evaluate reaction strategies that mitigate the studied position falsification attacks on vehicular platooning. Through our results, we demonstrate how mobile networks may benefit from employing rigorous methods to obtain higher assurance about their expected security properties. Furthermore, we show how considering increasing adversarial capabilities supports the assessment of these networks’ resilience and the design of new security mechanisms.