Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Design and Security of Collective Remote Attestation Protocols

Sharar Ahmadi, Jay Le-Papin, Liqun Chen, Brijesh Dongol, Sasa Radomirovic, Helen Treharne

TL;DR

CRA protocols face fragmentation across networks, topologies, and threat models. Catt provides a unified protocol model, formal threat/trust definitions, defense taxonomy, and a rigorous set of attestation properties, enabling systematic comparison and formal verification of CRA protocols via Tamarin, demonstrated on SIMPLE+. The work reveals that many protocols target Individual Attestation with asynchronous, weak guarantees and highlights gaps in group and synchronous attestation, suggesting concrete directions (e.g., DICE hardware, group strong attestation) to improve robustness and scalability in swarm environments.

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.

On the Design and Security of Collective Remote Attestation Protocols

TL;DR

CRA protocols face fragmentation across networks, topologies, and threat models. Catt provides a unified protocol model, formal threat/trust definitions, defense taxonomy, and a rigorous set of attestation properties, enabling systematic comparison and formal verification of CRA protocols via Tamarin, demonstrated on SIMPLE+. The work reveals that many protocols target Individual Attestation with asynchronous, weak guarantees and highlights gaps in group and synchronous attestation, suggesting concrete directions (e.g., DICE hardware, group strong attestation) to improve robustness and scalability in swarm environments.

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.
Paper Structure (40 sections, 4 figures, 4 tables)

This paper contains 40 sections, 4 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Contributions
  3. A Unified Protocol Model for CRA
  4. Device Integrity
  5. Attestation Target
  6. Trustworthiness of Verification
  7. Threat Models
  8. Software Attacks
  9. Physical Attacks
  10. Network Attacks
  11. Adversary Models
  12. Protection and Mitigation
  13. Defending Against Software Attacks
  14. Defending Against Physical Attacks
  15. Physical Attack Mitigation
  16. ...and 25 more sections

Figures (4)

  • Figure 1: Summary of roles and security properties in the Catt model. The prover(s) (yellow box) generate measurement(s) in response to request(s) from the initiator(s). Measurement(s) are verified by a range of mechanisms (green box) to generate result(s) that are sent to the relying party. We used dashed boxes to indicate that there are several design choices when selecting components that generate result(s) from measurement(s).
  • Figure 2: Lemma for IAS. The Lemma for IAW is obtained by omitting the cases (marked //Strong)
  • Figure 3: Lemma for Asynchronous Group Strong Attestation. Asynchronous Group Weak Attestation is similar, omitting the $att = unhealthy$ case.
  • Figure 4: Functions and equations for modelling binary OR and AND.

Theorems & Definitions (7)

  • Definition 1: Initiator Authentication (IA)
  • Definition 2: Weak Status Correctness
  • Definition 3: Strong Status Correctness
  • Definition 4: Asynchronous Weak/Strong Correctness
  • Definition 5: Synchronous (Weak/Strong) Correctness
  • Definition 6: Individual (A)Sync. Weak/Strong Att.
  • Definition 7: Group (A)Sync. Weak/Strong Att.