Security analysis of security protocol Swift implementations based on computational model

• 出版年: Tongxin xuebao
• 主要な著者: Bo MENG, Xudong HE, Jinli ZHANG, Lili YAO, Jintian LU
• フォーマット: 論文
• 言語: 中国語
• 出版事項: Editorial Department of Journal on Communications 2018-09-01
• 主題: security protocol; implementations security; Swift language; formal analysis; model extraction
• オンライン･アクセス: http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2018165/
• ISSN: 1000-436X

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.