计算机科学 ›› 2019, Vol. 46 ›› Issue (8): 206-211.doi: 10.11896/j.issn.1002-137X.2019.08.034

• 信息安全 • 上一篇    下一篇

基于概率模型的云辅助的轻量级无证书认证协议的形式化验证

夏奴奴, 杨晋吉, 赵淦森, 莫晓珊   

  1. (华南师范大学计算机学院 广州510631)
  • 收稿日期:2018-07-20 出版日期:2019-08-15 发布日期:2019-08-15
  • 通讯作者: 杨晋吉(1968-),男,博士,教授,主要研究方向为模型检测、协议验证,E-mail:yangjj@scnu.edu.cn
  • 作者简介:夏奴奴(1994-),女,硕士生,主要研究方向为模型检测、协议验证;赵淦森(1977-),男,博士,主要研究方向为云计算、大数据;莫哓珊(1993-),女,硕士生,主要研究方向为模型检测、协议验证

Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model

XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan   

  1. (School of Computing,South China Normal University,Guangzhou 510631,China)
  • Received:2018-07-20 Online:2019-08-15 Published:2019-08-15

摘要: 匿名WBANs通信技术是保护互联网用户和服务器间隐私的最有力手段之一,但匿名WBANs无证书认证协议的形式化验证仍是亟待解决的难题。采用概率模型检测的方法对一种基于云辅助的匿名WBANs的轻量级无证书认证协议建立离散时间马尔科夫链模型,在协议建模的状态迁移中加入了攻击率,重点对攻击率进行定量分析,用概率计算树逻辑对协议属性进行描述,利用PRISM概率模型检验工具对协议进行定量分析和验证,并且与SIP协议进行性能方面的对比。验证结果表明:在匿名WBANs通信环境下,云辅助的轻量级无证书认证协议各实体间所受攻击率对协议的不可否认性、时延性和有效性有不同程度的影响,控制好攻击率可以提高协议安全性,这对医疗服务质量和实时监测效率的提高以及远程医学的基本需求有着极大的意义。

关键词: PRISM, WBANs, 概率模型检测, 攻击率, 云辅助的轻量级无证书认证协议

Abstract: Anonymous wireless body area networks communication technology is one of the most powerful means to protect the privacy of Internet users and servers,but formal authentication of anonymous wireless body area networks certificateless authentication protocol is still a difficult problem to be solved.The method of probabilistic model detection is used to set up a discrete time Markov chain model based on a cloud-aided lightweight certificateless authentication protocol with anonymity for wireless body area networks.The attack rate is added to the state migration of the protocol modeling,and in particular,the attack rate was analyzed quantitatively.The protocol attributes are described with the probability calculation tree logic,the PRISM namely a probabilistic model testing tool was used for quantitative analysis and verification of the protocol,and the performance of the protocol was compared with the SIP protocol.The result shows that the attack rate between the entities of the cloud-aided lightweight certificateless authentication protocol has different influence on non-repudiation,time delay and effectiveness of the protocol under anonymous WBANs communication environment.The control of the attack rate can improve the security of the protocol.It is of great significance to the quality of medical services,the improvement of real-time monitoring efficiency and the basic needs of telemedicine

Key words: Attack rate, Cloud-aided lightweight certificateless authentication protocol, PRISM, Probabilistic model checking, Wireless body area networks

中图分类号: 

  • TP301
[1]ARMBRUST M,FOX A,GRIFFITH R,et al.A view of cloud computing[J].Communications of the ACM,2010,53(4):50-58.
[2]SMITH D B,MINIUTTI D,LAMAHEWA T A,et al.Propagation Models for Body-Area Networks:A Survey and New Outlook[J].IEEE Antennas & Propagation Magazine,2014,55(5):97-117.
[3]SABAHI F.Cloud computing security threats and responses [C]∥International Conference on Communication Software and Networks.IEEE,2011:245-249.
[4]CHEN T,KWIATKOWSKA M,PARKER D,et al.Verifying Team Formation Protocols with Probabilistic Model Checking[M]∥Computational Logic in Multi-Agent Systems.Springer Berlin Heidelberg,2011:190-207.
[5]LAPLANTE S,LASSAIGNE R,MAGNIEZ F,et al.Probabilistic abstraction for model checking:an approach based on property testing[J].Proceedings-Symposium on Logic in Computer Science,2002,8(4):30-39.
[6]HEATH J,KWIATKOWSKA M,NORMAN G,et al.Probabilistic Model Checking of Complex Biological Pathways[M]∥Computational Methods in Systems Biology.Springer Berlin Heidelberg,2006:32-47.
[7]FENG B,MA X,GUO C,et al.An Efficient Protocol With Bidirectional Verification for Storage Security in Cloud Computing[J].IEEE Access,2017,4(99):7899-7911.
[8]YANG B,FENG D G,QIN Y,et al.Secure Access Scheme of Cloud Services for Trusted Mobile Terminals using TrustZone[J].Journal of Software,2016,27(6):1366-1383.(in Chinese) 杨波,冯登国,秦宇,等.基于TrustZone的可信移动终端云服务安全接入方案[J].软件学报,2016,27(6):1366-1383.
[9]WU L B,ZHANG Y B,HE D B.Identity based double server ciphertext equivalence decision protocol in cloud computing[J].Computer Research And Development,2017,54(10):2232-2243.(in Chinese) 吴黎兵,张宇波,何德彪.云计算中基于身份的双服务器密文等值判定协议[J].计算机研究与发展,2017,54(10):2232-2243.
[10]SHEN J,GUI Z,JI S,et al.Cloud-aided lightweight certificateless authentication protocol with anonymity for wireless body area networks[J].Journal of Network & Computer Applications,2018,106:117-123.
[11]KWIATKOWSKA M,NORMAN G,PARKER D.Advances and challenges of probabilistic model checking[C]∥Communication,Control,and Computing.IEEE,2010:1691-1698.
[12]SHARIR M,PNUELI A,HART S.Verification of probabilistic programs[M].Society for Industrial and Applied Mathematics,1984.
[13]KWIATKOWSKA M,NORMAN G,PARKER D.PRISM 4.0:Verification of Probabilistic Real-Time Systems[J].Lecture Notes in Computer Science,2011,6806:585-591.
[14]LIU L,HASAN O,TAHAR S.Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL[J].Journal of Computer Science & Technology,2013,28(2):217-231.
[15]BALTAZAR P,MATEUS P,NAGARAJAN R,et al.Exoge- nous Probabilistic Computation Tree Logic[J].Electronic Notes in Theoretical Computer Science,2007,190(3):95-110.
[16]ROSTAMI M,BAGHERI E,LOTFI M.Cooperating the web services as distributed to create a Non- Repudiation service[J].International Proceedings of Economics Development & Research,2007,4526:9-19.
[17]WANG J,WANG Z,DING S,et al.Refined Jensen-Based Multiple Integral Inequality and Its Application to Stability of Time-Delay Systems[J].IEEE/CAA Journal of Automatica Sinica,2018,5(3):758-764.
[18]KREMER S.Formal Analysis of Optimistic Fair Exchange Pro- tocols[J].Journal of Software,2003,2004(3):509-521.
[19]WU L,ZHANG Y,WANG F.A new provably secure authentication and key agreement protocol for SIP using ECC[J].Computer Standards & Interfaces,2009,31(2):286-291.
[1] 马思琪, 车啸平, 于淇, 岳晨峰.
基于事件的虚拟现实用户体验评估方法研究
Event-based User Experience Evaluation Method for Virtual Reality Applications
计算机科学, 2021, 48(2): 167-174. https://doi.org/10.11896/jsjkx.200100065
[2] 周女琪, 周宇.
基于概率模型检测的Web服务组合多目标验证
Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking
计算机科学, 2018, 45(8): 288-294. https://doi.org/10.11896/j.issn.1002-137X.2018.08.052
[3] 刘爽, 魏欧, 郭宗豪.
基于概率模型检测和遗传算法的基因调控网络的无限范围优化控制
Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm
计算机科学, 2018, 45(10): 313-319. https://doi.org/10.11896/j.issn.1002-137X.2018.10.058
[4] 杜伊,何洋,洪玫.
概率模型检测在动态能耗管理中的应用
Application of Probabilistic Model Checking in Dynamic Power Management
计算机科学, 2018, 45(1): 261-266. https://doi.org/10.11896/j.issn.1002-137X.2018.01.046
[5] 郭宗豪,魏欧.
使用模型检测解决概率布尔网络优化控制
Optimal Control of Probabilistic Boolean Networks Using Model Checking
计算机科学, 2017, 44(5): 193-198. https://doi.org/10.11896/j.issn.1002-137X.2017.05.035
[6] 王晶 戎玫 张广泉 祝义.
基于概率模型检测的Web服务组合验证
Validation of Web Service Composition Based on Probabilistic Model Checking
计算机科学, 2012, 39(1): 120-123.
[7] 陈立斌 文英 董荣胜.
Ad Hoc网络中移动节点相邻概率的模型检测分析

计算机科学, 2006, 33(B12): 8-10.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!