Mechanized Verification of Security Properties of Transport Layer Security 1.2 Protocol with Crypto Verif in Computational Model

摘要

In modern society, many transactions have been processed through web-based applications. In order to protect those critical applications against attacks, Transport Layer Security (TLS) protocol has been implemented and widely deployed. The related literatures show that security analysis of TLS 1.2 protocol where cipher suite is RSA encryption has not been implemented with mechanized tool in computational model. Hence in this study, Blanchet calculus is used to analyze TLS 1.2 protocol where cipher suite is RSA encryption with mechanized tool crypto verif in computational model. The term, process and correspondence are used to model authentication in TLS 1.2 protocol where cipher suite is RSA encryption. The result shows that TLS 1.2 protocol where Cipher suite is RSA encryption has the pre master key confidentiality and authentication from server to client. The first mechanized analysis on TLS 1.2 protocol where Cipher suite is RSA encryption is implemented in computational model with active adversary in this study.