Reference implementation, evaluation framework and Tamarin theorems for our TPM 2.0 remote attestation protocol.