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

孟博; 何旭东; 张金丽; 尧利利; 鲁金钿

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

您当前的位置：

首页 >

文章列表页 >

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

论文Ⅲ：学术论文 | 更新时间：2024-06-05

- 基于计算模型的安全协议Swift语言实施安全性分析
- Security analysis of security protocol Swift implementations based on computational model
- 通信学报 2018年39卷第9期页码：178-190
- 作者机构：
  
  中南民族大学计算机科学学院，湖北武汉 430074
- 作者简介：
  
  [ "孟博（1974-），男，河北行唐人，博士，中南民族大学教授、硕士生导师，主要研究方向为安全协议和形式化方法。" ]
  [ "何旭东（1991-），男，湖北武汉人，中南民族大学硕士生，主要研究方向为安全协议实施安全。" ]
  [ "张金丽（1991-），女，湖北随州人，中南民族大学硕士生，主要研究方向为安全协议实施安全。" ]
  [ "尧利利（1993-），女，江西抚州人，中南民族大学硕士生，，主要研究方向为安全协议实施安全" ]
  [ "鲁金钿（1991-），男，土家族，湖南湘西人，中南民族大学硕士生，主要研究方向为形式化方法和安全协议逆向分析。" ]
- 基金信息：
  
  国家自然科学基金资助项目(61272497);湖北省自然科学基金资助项目(2014CFB249);湖北省自然科学基金资助项目(2018ADC150);中南民族大学中央高校基本科研业务费专项资金资助项目(CZZ18003);中南民族大学中央高校基本科研业务费专项资金资助项目(QSZ17007)
- DOI：10.11959/j.issn.1000-436x.2018165
  中图分类号： TP309
- 网络出版日期：2018-09，
  
  纸质出版日期：2018-09-25
- 稿件说明：
移动端阅览
孟博, 何旭东, 张金丽, 等. 基于计算模型的安全协议Swift语言实施安全性分析[J]. 通信学报, 2018,39(9):178-190.

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.
孟博, 何旭东, 张金丽, 等. 基于计算模型的安全协议Swift语言实施安全性分析[J]. 通信学报, 2018,39(9):178-190. DOI： 10.11959/j.issn.1000-436x.2018165.

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 ] .

浏览量

1135

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于CPN的安全协议形式化建模及安全分析方法

基于CPN的车载网络无证书匿名认证和密钥协商方案研究

基于身份认证的BACnet/IP分析与改进

室内定位隐私保护综述

SSMCI：以攻击者为中心的安全协议验证机制