Abstract： The Transport Layer Security(TLS) protocol is an important standard protocol for ensuring network transmission security, which realizes data encryption, data integrity, and identity verification. TLS protocol has been updated because there are many security vulnerabilities.Currently, the latest version is TLS1.3(RFC 8846) which has been released. Compared with the previous TLS1.2(RFC 5246), the content of the protocol has been greatly improved, improving security and transmission efficiency. In this paper, a hierarchical colored Petri net(HCPN) modelling method is used to model the TLS1.3 handshake protocol. At the same time, a Delov-Yao attack model is added, and we also analyze the state space report under the corresponding model. Finally,the experimental results show that the newly released pre-master key of the TLS1.3 handshake protocol has good confidentiality, and the identity authentication meets the security attribute requirements of the protocol specification. At present, there are few types of research on formal analysis methods of protocols in China. Therefore,This paper has theoretical guidance significance for other protocol analysis in terms of formal analysis methods of protocols.
Key words : TLS1.3；CPN Tools；TLS1.3 handshake protocol；formal analysis
