On the Design and Security of Collective Remote Attestation Protocols

TL;DR

This paper introduces Catt, a unifying framework for collective remote attestation protocols that systematically compares their security properties, based on an extensive analysis of 40 protocols and their adversary models.

Contribution

Catt provides a comprehensive classification and security property set for CRA protocols, enabling systematic comparison and verification of their security guarantees.

Findings

Developed a unifying framework for CRA protocols

Classified security aims of 40 CRA protocols

Verified SIMPLE+ protocol using Catt and Tamarin

Abstract

Collective remote attestation (CRA) is a security service that aims to efficiently identify compromised (often low-powered) devices in a (heterogeneous) network. The last few years have seen an extensive growth in CRA protocol proposals, showing a variety of designs guided by different network topologies, hardware assumptions and other functional requirements. However, they differ in their trust assumptions, adversary models and role descriptions making it difficult to uniformly assess their security guarantees. In this paper we present Catt, a unifying framework for CRA protocols that enables them to be compared systematically, based on a comprehensive study of 40 CRA protocols and their adversary models. Catt characterises the roles that devices can take and based on these we develop a novel set of security properties for CRA protocols. We then classify the security aims of all the studied protocols. We illustrate the applicability of our security properties by encoding them in the tamarin prover and verifying the SIMPLE+ protocol against them.