Formal analysis of improved EAP-AKA based on Protocol Composition Logic

A formal analysis based on PCL (Protocol Composition Logic) points out the vulnerability during the composition of EAP-AKA, and proposes an improved protocol EAP-AKA'. Based on DH protocol, the new protocol has session key secrecy, meanwhile, avoids the vulnerability to redirection attack and replay attack. Then a security analysis of the EAP-AKA' is made based on PCL, the analysis indicates that sub-protocols have SSA and key secrecy. According to the sequential rule, the precondition of a sub-protocol is preserved by the other one later in the chain, and each sub-protocol respects the invariant of the other, So EAP-AKA' is secure in the PCL mode.