Design and Security of the QR TPM (Dataset)

The datasets are SAPIC models and the output of the SAPIC-Tamarin toolchain used to create the final models towards verifying the security properties of the remote attestation service, as leveraged in the context of one of the envisioned FutureTPM use cases; namely, the Device Management where the focus is on the secure identification and management of network devices. The produced models are based on the ideal functionalities of TPM commands that have been defined through appropriate abstractions towards formally verifying the security properties of the executed protocols.