Modelling and analysing the TLS protocol using Casper and FDR

This paper analyses the TLS Handshake protocol in a progressive manner, by gradually building the protocol´s messages and message fields. Messages constituting the TLS protocol are described by Casper, a compiler for the analysis of security protocols. FDR, a model checking tool is then used to test whether the protocol achieves its goals. It has been shown that TLS achieves its security goals for the systems tested. By using this progressive approach of the TLS Handshake analysis, this paper identifies the importance of each message and message field to the overall achievement of the security goal of the TLS protocol. The study also shows that the TLS protocol contains much redundancy. A few important points that show how TLS has been carefully designed to thwart some attacks that have appeared in many of the previous security protocols are also emphasized.