Abstract: EAP-TLS is a security protocol defined under the 5G standard that provides key services in a specific IoT environment.However,the EAP-TLS protocol cannot provide mutual authentication between user equipment and the network.A protocol with design flaws will endanger the security of the system during operation.Therefore,it is a very necessary process to analyze its security before the implementation of the protocol,try to find potential flaws and improve them.This paper studies theformal model of EAP-TLS protocol and security properties based on Proverif,and verifies the security properties such as the mutual authentication between user equipment and network,confidentiality between KSEAF(security anchor key) and subscriber permanent identity(SUPI).Verification results find that there are some security flaws in the EAP-TLS protocol in terms of authentication under insecure channels,and the user equipment fails to authenticate the network.Analytical results further confirm the reasons of security flaws,and the corresponding attacks are also given.Finally,the possibility of improving security flaws is discussed based on asymmetric key encryption and random numbers in cryptography.

Key words: Authentication protocol, EAP-TLS, Formal verification, Proverif, Insecure channel