Information Technology Journal1812-56381812-5646Asian Network for Scientific Information10.3923/itj.2014.601.613MengBo NiuLeyuan YangYitong LiZimao 42014134In 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.]]>Bhargavan, K., C. Fournet, R. Corin and E. Zalinescu,2012Blanchet, B.,2008Chaki, S. and A. Datta,2009Fournet, C., K. Bhargavan, M. Kohlweiss, A. Pironti and P.Y. Strub,2013Jager, T., F. Kohlar, S. Schage and J. Schwenk,2012Jonsson, J. and B.S. Jr. Kaliski,2002Meng, B.,2011Morrissey, P., N.P. Smart and B. Warinschi,2008Ogata, K. and K. Futatsugi,2005Paterson, K.G., T. Ristenpart and T. Shrimpton,2011Paulson, L.C.,1999Wagner, D. and B. Schneier,1996