Remote attestation (RA) allows authentication of software components on untrusted systems by relying on a root of trust. Over the last years use of devices supporting remote attestation (RA) has been rising. Researchers have made several formal models to reason about RA, however, these models tend to stay fairly close to the implementations found in hardware. In this paper we devise a model, called pi_RA, that supports RA at a high level of abstraction by treating it as a cryptographic primitive in a variant of the applied pi-calculus.

To demonstrate the use of pi_RA, we use it to formalise and analyse the security of MAGE, an SGX-based framework that allows mutual attestation of multiple enclaves. This analysis is done by proving the security of a compiler, that incorporates MAGE to resolve problems with mutual attestation, from a language with named actors, pi_Actor, to pi_RA.