Generating Security Protocol Implementation Based On Computational Model

So far, the security of security protocol is still the focus of academic of computer security. But security analysis of security protocol rests on the level of abstract analysis of security protocol. This method of security verification cannot be successfully applied in our daily life. Furthermore, the abstract specification of security protocol ineluctably appears potential security vulnerability and it might be to bringing out many other threats to security. Many scholars made a lot of researches with the general security of security protocol implementation, such as array subscript beyond the range, memory leaks and type safety. The implementation of cryptography security in the security protocol would have a development tendency, but there are just a few research achievements in this field. Therefore, the main content of this thesis is the cryptography security of security protocol implementation.Mainly, there are two kinds of methods of analyzing security protocol: one is structure safety analysis under attack and the other one is formal analysis method. This article studies the security of security protocol at the code level, which has been researched to gain the implementation with more possesses stronger practicability and security in cryptography security. Firstly, to exploit and present cryptography security model of security protocol implementation, this paper studies probability symbol migration system. Secondly, exploring probabilistic process calculus Blanchet calculus and the method to establish security agreement abstract specification model. Base on the security protocol model, Blanchet calculus is used to study the eligibility of code conversion which establishes the mapping relationship between Java code and Blanchet calculus.This paper explores the method which generates Java code of security protocol(SP [Java]) from security protocol abstract specification model(SP[CV]) and abstract specification model for the mapping of different aspects such as role, goals and process. The main parts of software include lexical analyzer, parser, simplifier, translator, code generator and template. This paper illustrates the software development process through the introduction of software construction. Finally, CV2 JAVA is developed to generate Java code of security protocol. The paper uses the certification automation tool based on the calculation methods Crypto Verif to prove the authentication of security protocol and to validate the authentication of security protocol implementation. The automatic conversion software CV2 JAVA generates Java code from Blanchet calculus model of SSHV2 protocol which is the Java implementation code of SSHV2 protocol's specification process.SSHV2 protocol's implementation code is applied in development environment to prove the implementation code of protocol has identity authentication.