The worldwide implementation of Remote Identification (RID) regulations mandates unmanned aircraft systems (UAS), or drones, to openly transmit their identity and real-time location as plain text on the wireless channel. This mandate serves the purpose of accounting for and monitoring drone operations effectively. However, the current RID standard's plain-text transmission exposes it to cyberattacks, including eavesdropping, injection, and impersonation. The Drone Remote Identification Protocol (DRIP) has been proposed to enhance the security of RID. The DRIP ensures information secrecy and confidentiality by using unique session keys while guaranteeing the authenticity of messages and entities through digital signatures. These security features of DRIP make it a preferable alternative to the existing RID standard. However, the lack of verification regarding its security claims raises concerns about its performance in hostile conditions. This paper comprehensively analyzes the DRIP protocol's security features using Tamarin Prover, a formal security verification tool. With its automated reasoning capabilities, Tamarin Prover accurately identifies potential security vulnerabilities within the DRIP protocol while thoroughly verifying its conformance to security properties. Our investigation demonstrates that the DRIP protocol is susceptible to replay attacks. We strongly recommend the inclusion of message freshness components, reducing the lifespan of DET broadcasts, and incorporating a not-after timestamp that is set only a few minutes ahead of the current time. These measures enhance the protocol's defence against replay attacks and ensure message authenticity and Integrity.

Remote Attestation is emerging as a promising technique to ensure that some remote device is in a trustworthy state. This can for example be an IoT device that is attested by a cloud service before allowing the device to connect. However, flaws in the communication protocols associated with the remote attestation mechanism can introduce vulnerabilities into the system design and potentially nullify the added security. Formal verification of protocol security can help to prevent such flaws. In this work we provide a detailed analysis of the necessary security properties for remote attestation focusing on the authenticity of the involved agents. We extend beyond existing work by considering the possibility of an attestation server (making the attestation process involve three parties) as well as requiring verifier authentication. We demonstrate that some security properties are not met by a state-of-the-art commercial protocol for remote attestation for our strong adversary model. Moreover, we design two new communication protocols for remote attestation that we formally prove fulfil all of the considered authentication properties.

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.  

Remote attestation (RA) is emerging as an important security mechanism for cyber-physical systems with strict security requirements. Trusted computing at large and Trusted Execution Environments (TEEs) in particular have been identified as key technologies to enable RA since they ideally allow retaining some element of control over remote devices despite them being compromised at the OS level. Unfortunately, sometimes it is claimed that TEEs provide RA support without really substantiating how this support is provided. In this paper we build the assurance arguments for RA to carefully map how secure RA depends on underlying security properties and how these in turn can be provided by TEE capabilities. We base our security analysis of RA on existing literature on security requirements for RA and use Goal Structuring Notation (GSN) as the method to build the security arguments. Our analysis identifies the set of TEE properties (as described in the GlobalPlatform standard) that are needed to support RA, and which goals that cannot be mapped to TEE implementations, and therefore, require other forms of evidence for RA to be trusted at the top level.

Vehicular networks will enable a range of novel applications to enhance road traffic efficiency, safety, and reduce fuel consumption. As for other cyber-physical systems, security is essential to the deployment of these applications and standardisation efforts are ongoing. In this paper, we perform a systematic security evaluation of a vehicular platooning protocol through a thorough analysis of the protocol and security standards. We tackle the complexity of the resulting model with a proof strategy based on a relation on keys. The key relation forms a partial order, which encapsulates both secrecy and authenticity dependencies. We show that our order-aware approach makes the verification feasible and proves authenticity properties along with secrecy of all keys used throughout the protocol.

Microarchitectural attacks such as Meltdown and Spectre have attracted much attention recently. In this paper we study how effective these attacks are on the Genode microkernel framework using three different kernels, Okl4, Nova, and Linux. We try to answer the question whether the strict process separation provided by Genode combined with security-oriented kernels such as Okl4 and Nova can mitigate microarchitectural attacks. We evaluate the attack effectiveness by measuring the throughput of data transfer that violates the security properties of the system. Our results show that the underlying side-channel attack Flush+Reload used in both Meltdown and Spectre, is effective on all investigated platforms. We were also able to achieve high throughput using the Spectre attack, but we were not able to show any effective Meltdown attack on Okl4 or Nova.