Security analysis of security protocol Swift implementations based on computational model

Bo MENG; Xudong HE; Jinli ZHANG; Lili YAO; Jintian LU

doi:10.11959/j.issn.1000-436x.2018165

您当前的位置：

首页 >

文章列表页 >

Security analysis of security protocol Swift implementations based on computational model

Papers | 更新时间：2024-06-05

- Security analysis of security protocol Swift implementations based on computational model
- Journal on Communications Vol. 39, Issue 9, Pages: 178-190(2018)
- 作者机构：
  
  中南民族大学计算机科学学院，湖北武汉 430074
- 作者简介：
- 基金信息：
  
  The National Natural Science Foundation of China(61272497);The Natural Science Foundation of Hubei Province(2014CFB249);The Natural Science Foundation of Hubei Province(2018ADC150);The Central University Basic Business Expenses Special Funding for Scientific Research Project(CZZ18003);The Central University Basic Business Expenses Special Funding for Scientific Research Project(QSZ17007)
- DOI：10.11959/j.issn.1000-436x.2018165
  CLC： TP309
- Online First：2018-09，
  
  Published：25 September 2018
- 稿件说明：
移动端阅览
Bo MENG, Xudong HE, Jinli ZHANG, et al. Security analysis of security protocol Swift implementations based on computational model[J]. Journal on Communications, 2018, 39(9): 178-190.
DOI：

Bo MENG, Xudong HE, Jinli ZHANG, et al. Security analysis of security protocol Swift implementations based on computational model[J]. Journal on Communications, 2018, 39(9): 178-190. DOI： 10.11959/j.issn.1000-436x.2018165.

摘要

分析IOS平台上的安全协议Swift语言实施安全性，对保障IOS应用安全具有重要意义。首先对已有安全协议Swift语言实施进行分析，确定Swift语言子集SubSwift，并给出其BNF；其次基于操作语义，建立SubSwift语言到Blanchet演算的映射模型，主要包含SubSwift语言的语句、类型到Blanchet演算的语句及类型的映射关系与规则；再次根据SubSwift语言到Blanchet演算的映射模型，提出从安全协议SubSwift语言实施生成安全协议Blanchet演算实施方法；最后应用Antrl4工具和Java语言开发安全协议Blanchet演算实施生成工具SubSwift2CV，分析OpenID Connect协议、Oauth2.0协议和TLS协议的SubSwift语言实施安全性。

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

references

张焕国 , 韩文报 , 来学嘉 , 等 . 网络空间安全综述 [J ] . 中国科学:信息科学 , 2016 , 46 ( 2 ): 125 - 164 .

ZHANG H G , HAN W B , LAI X J , et al . Survey on cyberspace security [J ] . SCIENTIA SINICA Informationis , 2016 , 46 ( 2 ): 125 - 164 .

王世伟 . 论信息安全、网络安全、网络空间安全 [J ] . 中国图书馆学报 , 2015 ( 2 ): 72 - 84 .

WANG S W . On information security,network security and cyberspace security [J ] . Journal of Library Science in China , 2015 ( 2 ): 72 - 84 .

MIN K S , CHAI S W , HAN M . An international comparative study on cyber security strategy [J ] . International Journal of Security and its Applications , 2015 , 9 ( 2 ): 13 - 20 .

张焕国 , 吴福生 , 王后珍 , 等 . 密码协议代码执行的安全验证分析综述 [J ] . 计算机学报 , 2018 , 41 ( 2 ): 288 - 308 .

ZHANG H G , WU F S , WANG H Z , et al . A survey:security verification analysis of cryptographic protocols implementations on real code [J ] . Chinese Journal of Computers , 2018 , 41 ( 2 ): 288 - 308 .

孟博 , 张金丽 , 鲁金钿 . 基于计算模型的OpenID Connect协议认证性的自动化分析 [J ] . 中南大学民族大学学报（自然科学版） , 2016 , 35 ( 3 ): 123 - 129 .

MENG B , ZHANG J L , LU J T . Automatic analysis of authentication of OpenID Connect protocol based on the computational model [J ] . Journal of South-Central University for Nationalities (Natural Science Edition) , 2016 , 35 ( 3 ): 123 - 129 .

牛乐园 , 杨伊彤 , 王德军 , 等 . 计算模型下的SSHV2协议认证性自动化分析 [J ] . 计算机工程 , 2015 , 41 ( 10 ): 148 - 154 .

NIU L Y , YANG Y T , WANG D J , et al . Automatic analysis on authentication of SSHV2 protocol in computational model [J ] . Computer Engineering , 2015 , 41 ( 10 ): 148 - 154 .

AVALLE M , PIRONTI A , SISTO R . Formal verification of security protocol implementations:a survey [J ] . Formal Aspects of Computing , 2014 , 26 ( 1 ): 99 - 123 .

MENG B , HUANG C T , YANG Y T , et al . Automatic generation of security protocol implementations written in Java from abstract specifications proved in the computational model [J ] . International Journal of Network Security , 2017 , 19 ( 1 ): 138 - 153 .

MENG B , YANG Y T , ZHANG J L , et al . PV2Java:automatic generator of security protocol implementations written in Java language from the applied PI calculus proved in the symbolic model [J ] . International Journal of Security and its Applications , 2016 , 10 ( 11 ): 211 - 229 .

孟博 , 王德军 . 安全协议实施自动化生成与验证 [M ] . 北京 : 科学出版社 , 2016 .

MENG B , WANG D J . Automatic generation and verification of security protocols’ implements [M ] . Beijing : Science PressPress , 2016 .

雷新锋 , 宋书民 , 刘伟兵 , 等 . 计算可靠的密码协议形式化分析综述 [J ] . 计算机学报 , 2014 , 37 ( 5 ): 993 - 1016 .

LEI X F , SONG S M , LIU W B , et al . A Survey on computationally sound formal analysis of cryptographic protocols [J ] . Chinese Journal of Computers , 2014 , 37 ( 5 ): 993 - 1016 .

GOUBAULT L J , PARRENNES F . Cryptographic protocol analysis on real C code [C ] // International Workshop on Verification,Model Checking,and Abstract Interpretation . 2005 : 363 - 379 .

JURJENS J . Automated security verification for crypto protocol implementations:verifying the JESSIE project [J ] . Electronic Notes in Theoretical Computer Science , 2009 , 250 ( 1 ): 123 - 136 .

CHAKI S , DATTA A . ASPIER:an automated framework for verifying security protocol implementations [C ] // 22nd IEEE Computer Security Foundations Symposium . 2009 : 172 - 185 .

DUPRESSOIR F , GORDON A D , JÜRJENS J , et al . Guiding a general-purpose C verifier to prove cryptographic protocols [C ] // 24th IEEE Computer Security Foundations Symposium . 2011 : 3 - 17 .

BHARGAVAN K , GORDON A D . Modular verification of security protocol code by typing [C ] // ACM Sigplan-Sigact Symposium on Principles of Programming Languages . 2010 : 445 - 456 .

BACKES M , MAFFEI M , UNRUH D . Computationally sound verification of source code [C ] // 17th ACM Conference on Computer and Communications Security . 2010 : 387 - 398 .

BENGTSON J , BHARGAVAN K , FOURNET C , et al . Refinement types for secure implementations [J ] . ACM Transactions on Programming Languages and Systems , 2011 , 33 ( 2 ): 8 - 45 .

SWAMY N , CHEN J , FOURENT C , et al . Secure distributed programming with value-dependent types [C ] // 16th ACM Sigplan International Conference on Functional Programming . 2011 : 266 - 278 .

SWAMY N , HRIŢCU C , KELLER C , et al . Semantic purity and effects reunited in F* [C ] // 20th ACM SIGPLAN International Conference on Functional Programming . New York:ACM , 2015 :12.

SWAMY N , HRIŢCU C , KELLER C . Dependent types and multi-monadic effects in F* [C ] // 43rd annual ACM SIGPLANSIGACT Symp on Principles of Programming Languages . 2016 : 256 - 270 .

BHARGAVAN K , FOURNET C , GORDON A D , et al . Verified interoperable implementations of security protocols [J ] . ACM Transactions on Programming Languages and Systems , 2008 , 31 ( 1 ):5.

BHARGAVAN K , CORIN R , FOURNET C , et al . Automated computational verification for cryptographic protocol implementations [J ] . Unpublished draft,Oct , 2009 .

BHARGAVAN K , FOURNET C , CORIN R , et al . Cryptographically verified implementations for TLS [C ] // 15th ACM Conference on Computer and Communications Security . 2008 : 459 - 468 .

MIHHAIL A , GORDON A D , JÜRJENS J . Extracting and verifying cryptographic models from C protocol code by symbolic execution [C ] // 18th ACM Conference on Computer and Communications Security . 2011 : 331 - 340 .

AIZATULIN M , GORDON A D , JURJENS J . Computational verification of C protocol implementations by symbolic execution [C ] // 19th ACM Conference on Computer and Communications Security . 2012 : 712 - 723 .

BHARGAVAN K , BLANCHET K , KOBEISSI N . Verified models and reference implementations for the TLS 1.3 standard candidate [C ] // 38th IEEE Symp on Security and Privacy . 2017 :20.

BLANCHET B . A computationally sound mechanized prover for security protocols [J ] . IEEE Transactions on Dependable and Secure Computing , 2008 , 5 ( 4 ): 193 - 207 .

BLANCHET B , . An efficient cryptographic protocol verifier based on prolog rules [C ] // 14th IEEE Computer Security Foundations Workshop,Cape Breton . 2001 : 82 - 96 .

O'SHEA N , . Using ELYJAH to analyses Java implementations of cryptographic protocols [C ] // FCS-ARSPA-WITS'08 . 2008 : 211 - 223 .

LI Z M , MENG B , WANG D J , et al . Mechanized verification of cryptographic security of cryptographic security protocol implementation in JAVA through model extraction in the computational model [J ] . Journal of Software Engineering , 2015 , 9 ( 1 ): 1 - 32 .

唐朝京 , 鲁智勇 , 冯超 . 基于计算语义的安全协议验证逻辑 [J ] . 电子学报 , 2014 , 42 ( 6 ): 1179 - 1185 .

TANG Z J , LU Z Y , FENG C . A verification logic for security protocols based on computational semantics [J ] . Chinese Journal of Electronics , 2014 , 42 ( 6 ): 1179 - 1185 .

SONY Corporation . The Swift Programming Language [EB/OL ] .[2017-4-1 ]

TERENCE P . The definitive Antrl4 reference [M ] . USA : The Pragmatic BookshelfPress , 2012

SAKIMURA N , BRADLEY J , JONES M , et al . OpenID connect core 1.0 [EB/OL ] .[2017-1-10 ]

XU X D , NIU L Y , MENG B . Automatic verification of security properties of OAuth 2.0 protocol with CryptoVerif in computational model [J ] . Information Technology Journal , 2013 , 12 ( 12 ): 2273 - 2285 .

MENG B , NIU L Y , YANG Y T , et al . Mechanized verification of security properties of transport layer security 1.2 protocol with CryptoVerif in computational model [J ] . Information Technology Journal , 2014 , 13 ( 4 ): 601 - 613 .

Client library for OAuth2/OpenID Connect [EB/OL ] .[2016-10-1 ] .

Views

1827

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Formal modeling and security analysis method of security protocol based on CPN

Research on certificateless anonymous authentication and key agreement scheme of vehicle network based on CPN

Analysis and improvement of the BACnet/IP based on identity authentication

Survey on privacy protection indoor positioning

SSMCI:verification mechanism for security protocols centered on the attacker

Related Author

Xiang GONG

Jinze DU

Tao FENG

SU Chunhua

FENG Tao

ZHENG Lu

Jiafeng ZHU

Yongping KANG

Related Institution

School of Computer and Communication, Lanzhou University of Technology

Division of Computer Science, University of Aizu

School of Mechanical and Electrical Engineering, Lanzhou University of Technology

School of Computer and Communications, Lanzhou University of Technology

State Key Laboratory of Information Engineering in Surveying Mapping and Remote Sensing, Wuhan University

AI问答

⁰