计算机科学 ›› 2019, Vol. 46 ›› Issue (8): 206-211.doi: 10.11896/j.issn.1002-137X.2019.08.034
夏奴奴, 杨晋吉, 赵淦森, 莫晓珊
XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan
摘要: 匿名WBANs通信技术是保护互联网用户和服务器间隐私的最有力手段之一,但匿名WBANs无证书认证协议的形式化验证仍是亟待解决的难题。采用概率模型检测的方法对一种基于云辅助的匿名WBANs的轻量级无证书认证协议建立离散时间马尔科夫链模型,在协议建模的状态迁移中加入了攻击率,重点对攻击率进行定量分析,用概率计算树逻辑对协议属性进行描述,利用PRISM概率模型检验工具对协议进行定量分析和验证,并且与SIP协议进行性能方面的对比。验证结果表明:在匿名WBANs通信环境下,云辅助的轻量级无证书认证协议各实体间所受攻击率对协议的不可否认性、时延性和有效性有不同程度的影响,控制好攻击率可以提高协议安全性,这对医疗服务质量和实时监测效率的提高以及远程医学的基本需求有着极大的意义。
中图分类号:
[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. |
|