本文对5G鉴权认证协议EAP-AKA’进行了形式化分析,利用了TAMARIN形式化分析工具,主要验证了EAP-AKA’协议对安全锚点密钥KSEAF的安全属性满足情况,验证的安全属性包括机密性、完美前向保密性、Lowe鉴权性质。对EAP-AKA’协议的建模采用了3GPP的隐式鉴权和改进后的显式鉴权,其中EAPAKA_implicit表示隐式鉴权,EAPAKA_explicit表示显式鉴权。