Research on Formal Design of Key Exchange Protocol in Trusted Computing

The problem of trusted network connection (TNC) protocol extension is analyzed. Abiding by standards of trusted computing group, based on the security goals of key exchange in trusted computing environment, this paper proposes a key exchange protocol for TNC (KEPTNC) using authentication tests to construct the only transforming edge between the two communication entities. The secure properties of KEPTNC are formally proved with strand space model and authentication tests. KEPTNC can provide secure negotiation of session key and security association (SA), protection of endpoints´ identities, verification of platform integrity, and mutual authentication between the initiator and the responder. It needs only three messages and less computational load, and it is simple and efficient.