关键词: 认证密钥交换协议, 可证安全, TLS握手协议, 伪随机函数

Abstract: As a typical authentication and key exchange protocol, TLS handshake protocol could be analyzed under the framework of BR computational model. We provide computational analysis of this protocol and prove that, when implemented with pseudorandom function as message authentication algorithm and encryption scheme which satisfies IND-CCA standard, the TLS handshake protocol is indeed secure under computational model. The technicalities of our proof reveal insights regarding the relationship between formal and computational models of security protocol.