Abstract:There are numerous methods of network attacks, such as man-in-the-middle attacks, replay attacks, and DoS attacks, which are ways to gain improper benefits. The authentication and key agreement (AKA) is set up to provide a correct authentication portal for legitimate users and deny illegal access and attacks from attackers. AKA is the first line of security to protect mobile communications for higher quality of service. The AKA for 5G networks still has security problems in the actual environment, and it is still unknown whether the security features of AKA can meet the requirements. Therefore, this study proposes to use the method based on probabilistic model checking to build a discrete-time Markov chain model by modeling each protocol party entity of AKA for 5G networks. In the modeling process, the influence of external attacks is considered, and the attack rate is introduced to describe the degree of external influence. The studies of AKA for 5G networks are quantitatively analyzed through the attack rate, and the probabilistic computation tree logic is employed to describe the codes of the specifications for the a priori attributes. Experiments are conducted by the probabilistic model checking tool PRISM. The experimental results indicate that in the AKA model with the introduction of the attack rate, the attacks on each protocol party entity of AKA for 5G networks have different influences on the performance of the attribute specifications such as delay, validity, and confidentiality of the protocol. Therefore, the study of the impact of external network attacks on the security performance of the protocol has certain implications for strengthening the security performance of the protocol and its improvement, and it is of great significance to enhance the security features of AKA for 5G networks and protect the economic and information security of users.