Formally Verified Remote Attestation Protocols with Strong Authentication

Abstract: Most commodity processors available today provide hardware-supported security extensions. Remote attestation has been declared an important step towards providing security to users through such solutions, yet remote attestation has seen limited deployment in practice. For existing protocols, analysis of the protocol security is not always publicly available. This thesis utilises formal methods in order to investigate an existing remote attestation protocol in the form of Samsung Knox Enhanced Attestation V3 developed by Samsung for Samsung Knox devices. Requirements are formalised into verifiable security properties. Formal verification reveals a minor weakness when considering strong adversarial models that can control parts of the device through run-time attacks. Such adversarial models are generally stronger than what is typically considered for Knox devices. This thesis also develops general remote attestation protocols which remedy the found weakness with a simple mechanism. Our developed protocols are formally verified, showing that they are suitable for platforms with Trusted Execution Environments even when considering strong adversarial models.