A formal analysis about security and privacy with respect to 5G AKMA service.
There are two versions about our work and corresponding codes, which the former one is published in setta 2021(https://lcs.ios.ac.cn/setta2021/program.php), corresponding code is the script 5G_AKMA.spthy. According to the version change of Technical Specification, we modify and update our work and additional discuss the privacy issue, and the related work is implemented in the AKMA.spthy and Sim_privacy.spthy in the AKMA model(V17.4.0).