Security Analysis Of Security Protocol Web Implementations Based On Model Extraction

Security protocol Web implementation is an important part of cyber security.During Security protocol Web development,the programmer may introduce logical errors and coding errors that are not easily detected according to the abstract model specification of security protocol that is proven security,which leads to the very big gap between security protocol implementation and its abstract model specification.In order to address this problem,it is necessary to analyze the security protocol Web implementation to find out security issues in the implementation of the security protocol.This thesis uses the model extraction technology to extract the security protocol Applied PI calculus from browser implementation of security protocol in JavaScript language and Web server implementation of security protocol in Python language,then verifies its security through ProVerif.The main works of this thesis are as follows:(1)Present the research status and development trend of security analysis on security protocol implementation and discuss the security analysis method for security protocol implementation.(2)Analyze the core statements of the security protocol JavaScript language implementation and security protocol Python language implementation to define SubJavaScript,a subset of the JavaScript language,and SubPython,a subset of the Python language,and BNF[SubJavaScript] and BNF[SubPython],respectively.(3)Establish mapping models from SubJavaScript,SubPython to Applied PI calculus according to BNF [SubJavaScript] and BNF [Python] and BNF [Applied PI],respectively,which includes statement mapping and type mapping.(4)Use JavaCC to develop the model extraction tools SubJavaScript2 PV and SubPython2 PV based on the mapping models from SubJavaScript and SubPython to Applied PI calculus;SubJavaScript2PV and SubPython2 PV mainly is composed of six modules: lexical analyzer,parser,analyze abstract syntax tree,traversal abstract syntax tree,generate Applied PI calculus and model extraction tool interface design.(5)Apply SubJavaScript2 PV and SubPython2 PV to analyze security protocol of 51 Talk,mall management system,yintou Securities,MiCu Platform and GETWELL Clinical research management.The result shows that the password in the user login protocol of 51 Talk,the pukey-c and DESkey in the data transmission protocol of mall management system,the pwAndPhone in the user login protocol of yintou Securities,the pwandAgainPw in the register protocol of MiCu Platform and the pw in the user login protocol of GETWELL Clinical research management are confidential and no certified.