中文摘要：

通过应用π演算建模分析WTLS握手协议，得出其存在密钥泄露的缺陷，并加以改进。在密钥协商过程中使用幂运算处理随机数，并用RSA加密算法对所建立的预主密钥进行加密，以确保在私钥泄露的情况下，攻击者无法获取以后的会话密钥。利用ProVerif工具对改进后的WTLS握手协议进行验证，结果显示其满足后向安全性。

英文摘要：

the WTLS handshake protocol has a defect of key leakage by the application of model- ing and analysis based on the applied-π calculus. It is to ensure that when the keys leaked, the at- tackers cannot obtain the posteriori session keys by using the power to deal with the random number in both keys negotiation process and using RSA encryption algorithm to encrypt the transmission of the established preliminary master key. Using ProVerif to validate the improved WTLS handshake protocol, and the result shows that it has backward security.