Formal Modeling And Analysis Of 5G And Wireless Local Area Network Authentication Protocols

At present,mobile communication networks and wireless local area networks have become an indispensable part of life.In order to ensure the security of mobile communication networks and wireless local area networks,researchers have designed various authentication protocols to ensure the secure access of legitimate users.However,many authentication protocols were found to have significant security vulnerabilities years after they were put into use.Therefore,security analysis of authentication protocols is critical.Recently,several researchers used formal methods to analyze the security of authentication protocols in 5G networks and wireless local area networks.However,these works have different degrees of simplification in formally modeling protocol interaction details,attacker capabilities and security goals,which may lead to potential security vulnerabilities of the protocol being ignored.This dissertation uses the symbolic model in the formal method to analyze the security of the 5G EAP-TLS protocol in the 5G networks and the OWE protocol in the wireless local area networks,models the protocol interaction models in various modes,designs the attacker models in different scenarios,defines multiple security goals,analyzes the potential security risks of the protocol for the cases where the security goals cannot be met and proposes corresponding protection suggestions or revision schemes.The main works of this dissertation are as follows:1.Aiming at 5G networks,this dissertation proposes a fine-grained formal analysis scheme for the 5G EAP-TLS protocol.The scheme models the interaction details between the.protocol participants based on the protocol interaction flow described in the TS 33.501 standard document.This dissertation also models the Diffie-Hellman key negotiation model compared to the existing work which only models the RSA key negotiation model.The four participants of the protocol are also reduced according to the standard document.Moreover,this dissertation analyzes the security threats faced by the 5G EAP-TLS protocol,extends the attack capability of Dolev-Yao attacker model and proposes customized attacker models under different operation scenarios.This dissertation also defines the security goals that should be met during the operation of the protocol.This dissertation defines not only secrecy properties and authentication properties,but also forward secrecy properties and privacy properties compared to the existing work.2.Aiming at wireless local area networks,this dissertation proposes a fine-grained formal analysis scheme for the OWE protocol.Based on the 802.11 standard,the scheme reduces the three operating stages of the protocol and the counter mechanism used in the protocol interaction process.In order to reduce the details of protocol interactions in a more fine-grained way,this dissertation constructs the protocol interaction model in two modes:PMK caching mode and regular mode.Moreover,this dissertation also considers the scenario of malicious attackers participating in the protocol operation and proposes customized attacker models under various operating scenarios.This dissertation analyzes the security requirements of the OWE protocol in the absence of a clear definition of the security goals of the OWE protocol in the standards document and defines secrecy properties and forward secrecy properties that should be met during the operation of the protocol.3.This dissertation analyzes the potential security risks of the 5G EAP-TLS protocol and the OWE protocol and proposes corresponding protection suggestions or revision schemes.This dissertation uses the formal verification tool SmartVerif to verify the protocol interaction models,attacker models and security goals of the 5G EAP-TLS protocol and the OWE protocol.The experimental results show that in some specific attacker scenarios,part of the security goals of the 5G EAP TLS protocol and the OWE protocol are violated.In response to the violation of security goals,this dissertation summarizes 4 types of security risks of the 5G EAP-TLS protocol and 3 types of security risks of the OWE protocol,and proposes protection suggestions or revisions schemes.For the revised protocols,this dissertation uses the formal verification tool to verify and the experimental results show that the revised protocols satisfy the security goals defined in this dissertation.