Automatic Verification Of Authentication In Security Protocol Java Implementation In Computational Model

There is a growing concern over the protection of data privacy and the growingproblems of information security. Security protocol is the foundation of secure datatransmission in the field of network communications, and its correctness and validityhad become a focus of attention for our country. Formalization method is an importanttechnique of analysis and verification of security protocols. It involved: formal securityprotocols to establish abstract model of security protocol，use automated analysis toolsto prove Security properties of protocol. Formal analysis of security protocol obtained alot of achievements, and proposed multiple security models and developed variouskinds automated analysis tools.Although formal analysis of security protocol can prove the security properties ofsecurity protocol, but its analysis which build on the protocol abstract model is notpractical. Good practice dictates that implementing of security protocol which has beenproven right would even introduce new security problems, so it is inevitable to analyzethe security properties of security protocol’s cryptography implementing. There is littleresearch with security protocol implementing, automated model extraction andautomated code generation are two main technology. Based on automated modelextraction, we analyzed the implement of security protocol and extracted the securitymodel, and then generated the Blanchet calculus code. We use the automated proof toolnamed CryptoVerif which based on the calculation methods to prove the authenticationof source code. The main works was as follows:(1) A complete description of the formal analysis with security protocoltechniques and the formal techniques of security protocol implementation. We focus onthe theory of computation method and the techniques with extraction model.(2) We analysis Java grammar specification, establish the Java syntax subset ofsecurity protocol implementation. Then describe the Blanchet calculation which isformalized language base on computational method. We defined the syntax map fromJava’s syntax subset to Blanchet calculus.(3) Based on model extraction technology of security protocol code, we developmodel extraction tools SubJ2CV. The tool mainly analysis the morphology and syntax,and generate an abstract syntax tree for SubJ code of the protocol. Then we simplify theabstract syntax tree to extract the security model, and convert it to an abstract syntaxtree from Blanchet calculus to generate Blanchet calculus code.(4) We select an authentication protocol implemented in Java code, and applymodel extraction tools to obtain the Blanchet calculus form of the security model. Then,we call the automated analysis tools CryptoVerif to analysis authentication, so provethe authenticity of the protocol code.