改进的OpenID Connect协议及其安全性分析

doi:10.11772/j.issn.1001-9081.2017.05.1347

计算机应用 ›› 2017, Vol. 37 ›› Issue (5): 1347-1352.DOI: 10.11772/j.issn.1001-9081.2017.05.1347

改进的OpenID Connect协议及其安全性分析

鲁金钿, 尧利利, 何旭东, 孟博

中南民族大学计算机科学学院, 武汉 430074

收稿日期:2016-10-08 修回日期:2016-12-28 出版日期:2017-05-10 发布日期:2017-05-16
通讯作者: 孟博
作者简介:鲁金钿(1991-),男,湖南湘西人,硕士研究生,主要研究方向:网络协议形式化及逆向分析;尧利利(1993-),女,江西抚州人,硕士研究生,主要研究方向:数据存储安全;何旭东(1991-),男,湖北武汉人,硕士研究生,主要研究方向:安全体系结构与协议;孟博(1974-),男,河北石家庄人,教授,博士,主要研究方向:网络空间安全。
基金资助:
国家自然科学基金资助项目（61272497）；湖北省自然科学基金资助项目（2014CFB249）。

Improvement of OpenID Connect protocol and its security analysis

LU Jintian, YAO Lili, HE Xudong, MENG Bo

College of Computer Science, South-Central University for Nationalities, Wuhan Hubei 430074, China

Received:2016-10-08 Revised:2016-12-28 Online:2017-05-10 Published:2017-05-16
Supported by:
This work is partially supported by the National Natural Science Foundation of China (61272497), the Natural Science Foundation of Hubei Province (2014CFB249).

摘要/Abstract

摘要： OpenID Connect协议是最新的单点登录协议之一，已经广泛应用于用户身份认证领域，其安全性受到了人们的重点关注。为增强OpenID Connect协议的安全性，首先引入数字签名及非对称加密技术，对其进行改进，重点关注改进后协议的秘密性和认证性；其次基于符号模型，应用应用PI演算对改进的OpenID Connect协议进行形式化建模；然后为验证改进后协议的认证性和秘密性，分别使用非单射性和query对认证性和秘密性进行建模；最后把改进的OpenID Connect协议的应用PI演算模型转换为安全协议分析工具ProVerif的输入，应用ProVerif对其进行形式化分析。实验结果表明，改进后的OpenID Connect协议具有认证性和秘密性。

关键词: 非对称加密, 数字签名, 认证性, 符号模型, 形式化方法, ProVerif

Abstract: OpenID Connect protocol is widely used in identity authentication field and is one of the newest single sign-on protocols. In this paper, the digital signature and asymmetric encryption were used to improve OpenID connect protocol. The secrecy and authentication of the improved protocol were focused. And then the improved OpenID connect protocol was formalized with the applied PI calculus in the symbolic model, next the secrecy was modeled by query and the authentication was modeled by non-injective relations to test the secrecy and authentication of improved OpenID Connect protocol. Finally the formal model of the OpenID Connect protocol was transformed into the input of the automatic tool ProVerif based on symbol model. The results indicate that the improved OpenID Connect protocol is authenticable and secret.

Key words: aasymmetric encryption, digital signature, authentication, symbol model, formal method, ProVerif

中图分类号:

TP393.08

鲁金钿, 尧利利, 何旭东, 孟博. 改进的OpenID Connect协议及其安全性分析[J]. 计算机应用, 2017, 37(5): 1347-1352.

LU Jintian, YAO Lili, HE Xudong, MENG Bo. Improvement of OpenID Connect protocol and its security analysis[J]. Journal of Computer Applications, 2017, 37(5): 1347-1352.

参考文献

[1] 李雄.多种环境下身份认证协议的研究与设计[D]. 北京:北京邮电大学,2012:11-55.(LI X. Research and design on identity authentication protocol for multi-environments[D].Beijing:Beijing University of Posts and Telecommunications,2012:11-55.)
[2] 张焕国,韩文报,来学嘉,等. 网络空间安全综述[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.)
[3] OpenID Connect Core 1.0 incorporating errata set 1[EB/OL].[2016-04-16].http://OpenID.net/specs/OpenID-connect-core-1_0.html#toc.
[4] DICK H. The OAuth 2.0 authorization framework[EB/OL].[2016-02-15].http://tools.ietf.org/html/rfc6749.
[5] DAVID R, BRAD F. OpenID Authentication 2.0-Final, 2007[EB/OL].[2016-02-26].http://OpenID.net/specs/OpenID-authentication-2_0.html.
[6] 高焕芝.单点登录技术的研究[D]. 北京:北京邮电大学,2006:7-39.(GAO H Z. Research of single sign-on technology[D].Beijing:Beijing University of Posts and Telecommunications,2006:7-39.)
[7] LI W P, MITCHELLC J. Analysing the security of Google's implementation of OpenID connect[C]//Proceedings of 13th International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment. Berlin:Springer, 2016:357-376.
[8] ZHANG J L, LU J T, WAN Z Y, et al. Security analysis of OpenID connect protocol with cryptoverif in the computational model[C]//Proceedings of the 11th International Conference on P2P, Parallel, Grid, Cloud and Internet Computing. Berlin:Springer, 2016:925-934.
[9] BLANCHET B. Automatic proof of strong secrecy for security protocols[C]//Proceedings of the 2004 IEEE Symposium on Security and Privacy. Piscataway, NJ:IEEE, 2004:86-100.
[10] BHAVESH N B, MAITY S, HANSDAH R C. An authentication protocol for vehicular Ad Hoc networks with heterogeneous anonymity requirements[J]. International Journal of Space-Based and Situated Computing,2014, 4(1):1-14.
[11] 来学嘉,卢明欣,秦磊,等. 基于DNA技术的非对称加密与签名方法[J]. 中国科学:信息科学,2010,40(2):240-248.(LAI X J,LU M X,QIN L, et al. Asymmetric encryption and signature methods with DNA technology[J]. SCIENTIA SINICA Informationis, 2010,40(2):240-248.)
[12] 卓先德,赵菲,曾德明. 非对称加密技术研究[J]. 四川理工学院学报(自然科学版),2010,23(5):562-564.(ZHUO X D,ZHAO F,ZENG D M. Research of asymmetric encryption technology[J]. Journal of Sichuan University of Science & Engineering (Natural Science Edition),2010,23(5):562-564.)
[13] BLANCHET B. An efficient cryptographic protocol verifier based on Prolog rules[C]//Proceedings of the 14th IEEE Computer Security Foundations. Washington, DC:IEEE Computer Society, 2011:82-96.
[14] GUANGYE S, MOHAMED M. FASER (Formal and Automatic Security Enforcement by Rewriting) by BPA algebra with test[J]. International Journal of Grid and Utility Computing,2013,4(2/3):204-211.
[15] ABADI M, FOURNET C. Mobile values, new names, and secure communication[C]//Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York:ACM, 2001:104-115.
[16] BARENGHI A, GERARDO P, TERANEO F. Secure and efficient design of software block cipher implementations on microcontrollers[J]. International Journal of Grid and Utility Computing, 2013, 4(2/3):110-118.
[17] 冯超,张权,唐朝京. 计算可靠的Diffie-Hellman密钥交换协议自动证明[J]. 通信学报,2011,32(10):118-126.(FENG C,ZHANG Q,TANG C J. Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols[J].Journal on Communications,2011,32(10):118-126.)
[18] 孟博,张金丽,鲁金钿.基于计算模型的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.)

改进的OpenID Connect协议及其安全性分析

Improvement of OpenID Connect protocol and its security analysis

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	武鹏, 吴尽昭. 基于线性误差断言的推理方法[J]. 计算机应用, 2021, 41(8): 2199-2204.
[2]	杨龙海, 王学渊, 蒋和松. 改进SM2签名方法的区块链数字签名方案[J]. 计算机应用, 2021, 41(7): 1983-1988.
[3]	谷正川, 郭渊博, 方晨. 基于代理重加密的消息队列遥测传输协议端到端安全解决方案[J]. 计算机应用, 2021, 41(5): 1378-1385.
[4]	安鑫, 夏近伟, 杨海娇, 欧阳一鸣, 任福继. 基于离散控制器合成的异构多核系统资源管理方法[J]. 计算机应用, 2020, 40(6): 1698-1706.
[5]	秦楠, 马亮, 黄锐. 基于系统理论过程分析的软件安全性需求分析与验证方法[J]. 计算机应用, 2020, 40(11): 3261-3266.
[6]	韩德帅, 邢建春, 杨启亮, 李决龙. 自适应软件动态过程时间特性建模与验证方法[J]. 计算机应用, 2018, 38(3): 799-805.
[7]	周致成, 李立新, 李作辉. 基于区块链技术的高效跨域认证方案[J]. 计算机应用, 2018, 38(2): 316-320.
[8]	徐明迪, 高杨, 高雪原, 张帆. 满足对应性属性的平台配置证明[J]. 计算机应用, 2018, 38(2): 337-342.
[9]	曾小飞, 卢建朱, 王洁. 传感器节点相互协作的广播认证[J]. 计算机应用, 2016, 36(8): 2219-2224.
[10]	李云, 陈庞森, 孙山林. 基于近场通信认证的无线局域网无线接入协议的安全性设计[J]. 计算机应用, 2016, 36(5): 1236-1245.
[11]	左黎明, 陈仁群, 郭红丽. 可证安全的基于身份的签密方案[J]. 计算机应用, 2015, 35(3): 712-716.
[12]	杜桂颖, 黄振杰. 高效的基于证书可验证加密签名方案[J]. 计算机应用, 2015, 35(2): 407-411.
[13]	王倩, 郑东, 任方. 基于编码的盲签名方案[J]. 计算机应用, 2015, 35(10): 2867-2871.
[14]	莫礼平周恺卿. 方块苗文动态构造方法的形式化描述[J]. 计算机应用, 2014, 34(3): 861-864.
[15]	叶翔徐展胡翔刘丹. 低成本有源RFID双向认证加密方案[J]. 计算机应用, 2014, 34(2): 456-460.