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