关键词: 可信计算，可信网络，可信连接架构，形式化验证，进程代数

Abstract: TCA (trusted connection architecture) is the solution of trusted network of China. TCA specifies the entitics, the interfaces of information exchange among these entities and the behaviors of information exchange among these entities when a terminal with TPCM (trusted platform control module) connects to a trusted network. We give the process algebra description of each entity's state transferring based on the abstraction of the information exchange behaviors of entities in TCA. Formal verification of trusted connection architecture is done by use of axioms of process algebra. Verification result exhibits that TCA has desired external behavior.

Key words: Trusted computing, Trusted network,TCA,Formal verification,Process algebra