Modern attestation based on Trusted Execution Environments (TEEs) can significantly reduce the risk of secret compromise, allowing users to securely perform sensitive computations such as running cryptographic protocols for authentication across security critical services. However, this has made TEEs a high-value target, driving an arms race between novel compromise attacks and continuous TEEs updates. Ideally, we want to achieve Post-Compromise Security (PCS): even after a TEE compromise, we can update it back into a secure state. However, at the same time, we would like to guarantee the privacy of users, in particular preventing providers (such as Intel, Google, or Samsung) or services from tracking users across services. This requires unlinkability, which seems incompatible with standard PCS healing mechanisms. In this work, we develop TokenWeaver, the first privacy- preserving post-compromise secure attestation method with automated formal proofs for its core properties. Our construction weaves together two types of token chains, one of which is linkable and the other is unlinkable. We provide the formal models based on the Tamarin and DeepSec provers, including protocol, security properties, and proofs for reproducibility, as well as a proof-of-concept implementation in python that shows the simplicity and applicability of our solution.
IEEE Symposium on Security and Privacy (S&P)
2024-10-09
2024-10-09