The Research On Methods Of Formalizing Anonymity For Security Protocols Based On PCL

At present, a large number of protocols have been designed, how to verify the security of protocols is an important research field. In order to analyze protocols, different formal methods are proposed by cryptographies such as modal logic, model checking logic and theorem proving method. However most of the formal methods are applied to verify authentication and confidentiality, formal analysis of other security properties such as the anonymity is still in its infancy.This paper tries to put forward a method of formalizing anonymity for security protocols based on PCL in order to further improve the theory of formal analysis of protocols and better analyze anonymity. Combining observational equivalence with PCL, this paper proposes a method of formalizing anonymity and applies it to a specific network protocol to verify the feasibility and correctness of the new method.Firstly, this paper describes the background and significance of the study tor formalizing anonymity for protocols, and points out some existent shortcomings of the present study, and introduces the basic concepts of security protocols, anonymity and formalization, and summarizes three main types of formalization methods, and describes and analyzes the important formalization method, PCL model.Sencondly, in order to solve the problem PCL cannot formalize anonymity, this paper proposes a new method of formalizing anonymity. In view of the messages involved in protocols, messages of PCL were divided into three kinds of plaintext, ciphertext and composition. Combining the analytical ability of observers with the above messages, five equivalence theorems and the semantics of equivalent messages are defined. Combining the equivalent messages with the definition of traces, the concept of equivalent traces is defined. Based on the equivalent traces, sender anonymity, recipient anonymity and relation anonymity are defined.Finally, in order to validate the feasibility and correctness of the new method in the formal analysis of the protocol, this paper takes Direct Anonymous Attestation (DAA) as an example. The two sub-protocols of DAA are formalized to reason the anonymity using the new method, the result of which demonstrates DAA satisfies anonymity and verifies the correctness and feasibility of the new method.