Attachment Protocol Linkability Attack Verification Based On Pro Verif Extension Tool

The security protocol is the basis for ensuring that information interaction is carried out under security conditions.However,designed and deployed security protocols are often flawed.Therefore,a set of schemes is needed to ensure that the security protocol is secure.Nowadays,there are several strategies to verification security protocols,consisted of logical analysis methods,theorem proving methods and formal verification strategies,among which formal verification is generally accepted.This thesis uses formal methods to verify security protocols.In this thesis,formal methods are used to verify the security of Fifth Generation Mobile Communication System(5G)attachment request process and several other security protocols.Failure of attachment process in 5G attachment request may cause linkability attack,which violates anonymity and unlinkability,while in ProVerif it is impossible to automatically verify these two attributes.In order to automatic verification anonymity and,in this thesis extended a new tool based on ProVerif.The extension tool automatic constructs two attributes of unlinkability and anonymity.Then use the ProVerif tool to verify the protocol linkability attack.The experimental results show that the failed attachment request security policy in the 5G attachment protocol can resist the linkability attack,and the extended tool can also automatically verify linkability attack problem the security protocol.This thesis shows that several groups of protocols are secure through formal methods tool ProVerif verification,and also shows the advantages of formal verification.The formal verification tool ProVerif is extended to verify linkability attacks automatically.The verification of the tool also proves that the protocol achieves the purpose of resisting linkability attack.