A Symbolic Model for Systematically Analyzing TEE-Based Protocols

Trusted Execution Environment (TEE) has been widely used as an approach to provide an isolated storage and computation environment for various protocols, and thus security features of TEE determine how to design these protocols. In practice, however, new TEE-based protocols are often designed empirically, and a lack of comprehensive analysis against real threat models easily results in vulnerabilities and attacks. Unlike most past work focusing on communication channels or secure enclaves, we present a formal model for TEE-based protocols, which includes a detailed threat model taking into account attacks from both network and TEE-based platforms together with a scalable multiset-rewriting modelling framework instantiated by Tamarin. Based on the proposed threat model and formalism, we use Tamarin to systematically and automatically analyze related offline and web-based protocols considering all combination of threats. The results and comparison highlight the protocols’ advantages and weaknesses inherited from TEE-based platforms. Moreover, we also capture some vulnerabilities that are difficult to be found under the traditional threat model and propose corresponding fixes.