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.

翻译：集体远程证明（CRA）是一种旨在高效识别（异构）网络中受感染（通常是低功耗）设备的安全服务。过去几年中，CRA协议提案呈现快速增长态势，展现出基于不同网络拓扑、硬件假设及其他功能需求的多样化设计。然而，这些协议在信任假设、敌手模型和角色描述方面存在差异，导致难以统一评估其安全保障。本文提出Catt——一个用于CRA协议的统一框架，该框架基于对40个CRA协议及其敌手模型的系统性研究，实现了协议间的标准化比较。Catt明确了设备可能承担的角色类型，并据此建立了一套新颖的CRA协议安全属性体系。我们对所有研究协议的安全目标进行了分类，并通过在Tamarin验证器中形式化编码这些安全属性，对SIMPLE+协议进行了验证，从而展示了该安全属性体系的实际适用性。