标题：Mechanized Verification of Cryptographic Security of Cryptographic Security Protocol Implementation in JAVA through Model Extraction in the Computational Model
摘要：Many security protocols have been designed, implemented and deployed in various types of information systems in the last several decades. Hence, the security properties of security protocols have received serious attention. The hot issue has changed from the analysis of security properties of security protocol abstract specifications to the analysis of security properties of security protocol implementations. In this study, the model of analysis and verification of cryptographic security in security protocol implementations is presented. Therefore, in addition, the SubJAVA language is presented which is a subset of JAVA language and an automatic verifier SubJAVA2CV is developed which is able to transform security protocols written in SubJAVA to the security protocol abstract specification written in Blanchet calculus in the computational model. Finally, we use the automatic verifier SubJAVA2CV and CryptoVerif to analyze the authentication of a Needham-Schroeder protocol implementation in SubJAVA.
