Security analysis of security protocol Swift implementations based on computational model |
| |
Authors: | Bo MENG Xudong HE Jinli ZHANG Lili YAO Jintian LU |
| |
Affiliation: | College of Computer Science,South Central University For Nationalities,Wuhan 430074,China |
| |
Abstract: | 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. |
| |
Keywords: | security protocol implementations security Swift language formal analysis model extraction |
|
| 点击此处可从《通信学报》浏览原始摘要信息 |
|
点击此处可从《通信学报》下载全文 |
|