Design And Formal Verification Of Trusted Channel Protocols

Currently the security of most networks relies on secure channel technologies, such as SSH and IPSec, to protect confidential information on the Internet. However, as the attacking technology of malicious users becomes more sophisticated, the modern PC systems are more vulnerable to malicious code attacks, illegally information stealing and other security threats, which make the attack through damaging the terminals. Trusted computing can enhance the security level of the secure channel technologies by improving the security of terminals. Trusted computing uses the Trusted Platform Module (TPM) as the roots of trust for storage and measurement, aiming to apply hardware enforcement mechanisms to provide an adequate foundation for building a high-assurance trusted platform. We provide a scheme of trusted channel protocol. The scheme combines remote attestation of Trusted Computing with the procedure of establishing a secure connection. The proposed method not only deals with the problem of communicating with unknown endpoint security in secure channel protocol, but also ensures the confidentiality of information on the Internet.We first study the fundamentals of Trusted Computing, especially the Integrity Measurement mechanism which is the core and basis of Trusted Computing. With the comparisons of security protocol, we choose the SSH protocol as the secure channel protocol. We also analyze OpenSSH handshake connection, and design the procedure of establishing a trusted secure connection and exchanging a session key.In order to verify the security feature of the proposed scheme, we also study formal methods of verifying security protocols. Through the counterexample from the symbolic model checking tool, NuSMV, which verifies the two abstraction of our scheme, we improve the key exchanging protocol. In the end we propose a Trusted SSH protocol framework which holds the transparency of remote attestation in key exchanging algorithm and the confidentiality of platform information on the Internet.