Research On Automatic Generation Of Security Protocol Implementations Based On The Symbolic Model

In today's rapid development of information technology,more and more people use the Internet to obtain information,more and more personal information will be submitted to the network,the popularity of social chat and some network applications makes people attention information security more and more.Security protocol is an important part of information security,it is composed of two or more parties,conducting a series of messages exchanged to achieve some intended purpose.Formal analysis of security protocol,which uses formal modeling method of analysis to verify the security of security protocols,including confidentiality and authentication,and so on.Only prove security protocols' Abstract Security is not enough,during implement the security protocols with the specific codes,many problems will come out,such as memory leaks and other potential safety problems.So a large number of scholars began security protocols' implement(code-level)security research,implement security has also become the important development direction of security protocols.This paper completed a number of tasks in the implementation of security research:(1)Research the code transformation technology,list the syntax transform mapping between applied PI calculus and Java language.(2)Lexical analysis and syntax analysis the applied PI calculus,generate its grammatical structure and a syntax tree;Turn applied PI calculus syntax tree into Java syntax tree,finally turn the applied PI calculus with security into Java code;(3)Develop transformation tools PV2 JAVA,which converse applied PI calculus codes into Java codes;(4)Using applied PI calculus to formally analyze the application of security protocols,and analyze its authentication with ProVerif.Then use PV2 JAVA to transform protocols' applied PI calculus implementation to Java implementation,adjust the Java codes and run in eclipse,analysis the authentication,and then compare the result and certification result in ProVerif to prove the correctness of the transformation.