中文摘要：

针对WTLS握手协议中的特殊密码原语,用等值理论定义了椭圆曲线DH密钥交换原语,用可信机构颁发数字证书的方式定义了数字证书原语。并在密码原语定义的基础上建立了WTLS握手协议的形式化模型,最后用Pro Verif工具分析了协议的秘密性和认证性。结果表明WTLS握手协议满足其安全性说明。

英文摘要：

According to the special cryptographic primitives of WTLS handshake protocol,ECDH key agreements using equation theories and digital certificates using aprocess model of a Certification Authority issuing digital certificates are defined in this paper.Based on those definitions,formal models for WTLS handshake protocol are built.In the last,Pro Verif tool is used to verify security and authentication of the protocol.Results show that WTLS handshake protocol can meet its security statement.