Formal Verification Of Security Protocols Implementation By Java

Analysis and verification of security protocols plays a important part of the field ofinformation security. At present,the formal methods of analysis and verification ofsecurity protocols mainly focus on the abstract specification which is poor inpracticality,which involves less focus on analysis and verification of security protocolwhich emphasis on practicality;static program verification technology mainlyconcentrated in program correctness,what rarely associated with the code ofcryptography security.This article will be combination of secutity protocol analysis andverification and static program verification techniques to analyze and verify securityprotocols implementation by Java.The results of this research has a strong theoreticalsignificance and application value.The main work in this dissertation are summarized as following:1.A complete overview of the analysis and verification of security protocols,indicating that the formal analysis of the need for a formal analysis of the model and adetailed description of the methods of formal analysis and verification.2.Explore the formal description of the Java language, specifically the Javastatements and expressions to the mapping of the application of PI calculation statement.At the same time, introduce the program static analysis methods and how to pretreatprogram by the syntax tree.3.First,explore the extraction method of abstract model of Java program and themapping of Java program to the application of PI calculus;and then apply the first-ordertheorem proving ProVerif verify the cryptography security of Needham-Schroederprotocol implementation by Java.