基于计算模型的安全协议Swift语言实施安全性分析  

Security analysis of security protocol Swift implementations based on computational model

作　　者：孟博[1] 何旭东[1] 张金丽[1] 尧利利 鲁金钿 MENG Bo;HE Xudong;ZHANG Jinli;YAO Lili;LU Jintian(College of Computer Science,South Central University For Nationalities,Wuhan 430074,China)

机构地区：[1]中南民族大学计算机科学学院

出　　处：《通信学报》2018年第9期178-190,共13页Journal on Communications

基　　金：国家自然科学基金资助项目(No.61272497);湖北省自然科学基金资助项目(No.2014CFB249;No.2018ADC150);中南民族大学中央高校基本科研业务费专项资金资助项目(No.CZZ18003;No.QSZ17007)~~

摘　　要：分析IOS平台上的安全协议Swift语言实施安全性,对保障IOS应用安全具有重要意义。首先对已有安全协议Swift语言实施进行分析,确定Swift语言子集SubSwift,并给出其BNF;其次基于操作语义,建立SubSwift语言到Blanchet演算的映射模型,主要包含SubSwift语言的语句、类型到Blanchet演算的语句及类型的映射关系与规则;再次根据Sub Swift语言到Blanchet演算的映射模型,提出从安全协议Sub Swift语言实施生成安全协议Blanchet演算实施方法;最后应用Antrl4工具和Java语言开发安全协议Blanchet演算实施生成工具SubSwift2CV,分析OpenID Connect协议、Oauth2.0协议和TLS协议的SubSwift语言实施安全性。Analysis of security protocol Swift implementations in IOS platform is important to protect the security of IOS applications.Firstly,according to the security protocol Swift implementations,the SubSwift language,which was a subset of Swift language,was widely used in IOS system,and its BNF were specified.Secondly,the mapping model from SubSwift language to Blanchet calculus based on the operational semantic was presented which consisted of mapping rules,relationship from the statements and types in SubSwift language to Blanchet calculus.And then,a method of generating security protocol Blanchet calculus implementations from SubSwift language implementations was developed.Finally,security protocol Blanchet calculus implementation generation tool SubSwift2CV was developed with Antrl4 and Java language.At the same time,OpenID Connect,Oauth2.0 and TLS security protocol SubSwift language implementations were analyzed with SubSwift2CV and CryptoVerif.

关 键 词：安全协议 实施安全性 Swift语言 形式化分析 模型抽取 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]