Formal Verification of TCG Remote Attestation Protocols Based on Process Algebra

Remote attestation protocol of TCG (Trusted Computing Group) is the earliest remote attestation solution for trusted computing. Two forms of TCG remote attestation are analyzed: direct remote attestation protocol and remote attestation with trusted third party protocol. And the abstract models of the above two forms are presented in which interacting channels between the whole system and the outside environment are treated as exterior channels and interacting channels between parts of the system are treated as inner channels. Based on these abstract models, we provide the process algebra-based formal descriptions, in which every part involved in the protocols is described by a process term to capture the state transitions of the system part, and we put these process terms into parallel to get the whole formal systems. Then we conduct the related formal verifications of the parallel formal system based on the axioms of process algebra. The verification results show that the formal systems of two protocols exhibit desired external behaviors.