Formal Verification of Establishment of Chain of Trust in Trusted Computing

For formal verification for establishment of chain of trust,the process algebra description of each entity's state transferring was given based on the abstraction of the establishing process of trusted platform control modeule( TPCM)-based chain of trust. Formal verification was conducted by use of axioms of process algebra. Verification result exhibits that the system has desired external behavior.