Formally-verified Security against Forgery of Remote Attestation using SSProve

TL;DR

This paper provides a formal, mechanized security proof for remote attestation protocols against forgery, using the SSProve framework and the Rocq Prover, establishing a rigorous security foundation.

Contribution

It introduces the first formal mechanization of RA security properties using StateSeparating Proofs in Rocq Prover, reducing RA security to digital signature security.

Findings

Rocq Prover successfully verifies security against forgery.

RA security is reduced to digital signature security.

Primitives of RA are proven secure based on signature security.

Abstract

Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous mechanized definition of its security properties in one of the strongest models, i.e., the semantic model. Such a mechanization requires the concept of StateSeparating Proofs (SSP). However, SSP was only recently implemented as a foundational framework in the Rocq Prover. Based on this framework, this paper presents the first mechanized formalization of the fundamental security properties of RA. Our Rocq Prover development first defines digital signatures and formally verifies security against forgery in the strong existential attack model. Based on these results, we define RA and reduce the security of RA to the security of digital signatures. Our development provides evidence that the RA protocol is secure against forgery. Additionally, we extend our reasoning to the primitives of RA and reduce their security to the security of the primitives of the digital signatures.