文章基本信息

标题：Mechanized Verification of Cryptographic Security of Cryptographic Security Protocol Implementation in JAVA through Model Extraction in the Computational Model
本地全文：下载
作者：Zimao Li ; Bo Meng ; Dejun Wang 等
期刊名称：Journal of Software Engineering
印刷版ISSN：1819-4311
电子版ISSN：2152-0941
出版年度：2015
卷号：9
期号：1
页码：1-32
DOI：10.3923/jse.2015.1.32
出版社：Academic Journals Inc., USA
摘要：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.