As a critical component of the security architecture of 5G network, the authentication protocol plays a role of the first safeguard in ensuring the communication security, such as the confidentiality of user data. EAP-TLS is one of such protocols being defined in the 5G standards to provide key services in the specific IoT circumstances. This protocol is currently under the process of standardization, and it is vital to guarantee that the standardized protocol is free from any design flaws, which may result in severe vulnerabilities and serious consequences when implemented in real systems. However, it is still unclear whether the proposed 5G EAP-TLS authentication protocol provides the claimed security guarantees. To fill this gap, we present in this work a comprehensive formal analysis of the security related properties of the 5G EAP-TLS authentication protocol based on the symbolic model checking approach. Specifically, we build the first formal model of the 5G EAP-TLS authentication protocol in the applied pi calculus, and perform an automated security analysis of the formal protocol model by using the ProVerif model checker. Our analysis results show that there are some subtle flaws in the current protocol design that may compromise the claimed security objectives. To this end, we also propose and verify a possible fix that is able to mitigate these flaws. To the best of our knowledge, this is the first thorough formal analysis of the 5G EAP-TLS authentication protocol.

Focusing on non-iterative approaches in training feed-forward neural networks, this special issue includes 12 papers to share the latest progress, current challenges, and potential applications of this topic. This editorial presents a background of the special issue and a brief introduction to the 12 contributions.