Formal verification of Remote Attestation protocols in a Fog Computing Architecture

This work of thesis is related to the European project called Rainbow. Rainbow aims to provide a secure fog computing platform for managing heterogeneous IoT devices. Fog computing is a cloud infrastructure that consists in devices connecting to a cloud, but instead of forwarding data to the centre of the cloud, much of the processing is done at the edges. In this type of architecture, there are three main actors: Orchestrator, Fog Nodes, TPM(Trusted Platform Module). Since a great number of devices (Fog Nodes) is involved in this scenario, it is important that these devices can always be considered trusted: the process to check their correctness is called Remote Attestation. The objective of this thesis is to model and verify Remote Attestation protocols, designed for the Rainbow platform, to check if they can be considered secure. The correctness and security of remote attestation protocols has been analysed using the Formal Verification technique, which is an a-priori security verification of a mathematical model. The tool used to symbolically model and analyse the protocols is the Tamarin Prover. In particular, the protocols are modelled using a set of rules, described by facts that yield traces; security properties to be verified are modelled using lemmas, which capture the produced traces. Tamarin prover, given the model as input, automatically proves the correctness of the protocol, in an unbounded number of sessions and in presence of a Dolev-Yao(DY) adversary, an attacker with full control over the network. The protocols modelled and analysed are related to two kind of remote attestation processes: Attestation by Quote and Oblivious Remote Attestation. The first one consists is a protocol handled by the Orchestrator, who compares the values of its virtual PCRs (registers) with the one sent upon request by the node in a structure called Quote, to verify their correctness. The second one, the Oblivious Remote Attestation, is a process based on the usage of an Attestation Key bound to the node that attests that it can be considered trusted. The security properties that a remote attestation protocol should guarantee during its execution have been modelled using lemmas, which describe the properties to verify using the tool. The main lemmas describing the security properties analysed in this work are secrecy, authentication, aliveness, injective agreement and functional correctness. The results of the formal verification of the remote attestation protocols are described in this work of thesis, showing the traces produced by the Tamarin prover in interactive mode.