| 基于概率模型的云辅助的轻量级无证书认证协议的形式化验证 |
| |
| 引用本文： | 夏奴奴,杨晋吉,赵淦森,莫晓珊. 基于概率模型的云辅助的轻量级无证书认证协议的形式化验证[J]. 计算机科学, 2019, 46(8): 206-211 |
| |
| 作者姓名： | 夏奴奴 杨晋吉 赵淦森 莫晓珊 |
| |
| 作者单位： | 华南师范大学计算机学院 广州 510631;华南师范大学计算机学院 广州 510631;华南师范大学计算机学院 广州 510631;华南师范大学计算机学院 广州 510631 |
| |
| 摘 要： | 匿名WBANs通信技术是保护互联网用户和服务器间隐私的最有力手段之一,但匿名WBANs无证书认证协议的形式化验证仍是亟待解决的难题。采用概率模型检测的方法对一种基于云辅助的匿名WBANs的轻量级无证书认证协议建立离散时间马尔科夫链模型,在协议建模的状态迁移中加入了攻击率,重点对攻击率进行定量分析,用概率计算树逻辑对协议属性进行描述,利用PRISM概率模型检验工具对协议进行定量分析和验证,并且与SIP协议进行性能方面的对比。验证结果表明:在匿名WBANs通信环境下,云辅助的轻量级无证书认证协议各实体间所受攻击率对协议的不可否认性、时延性和有效性有不同程度的影响,控制好攻击率可以提高协议安全性,这对医疗服务质量和实时监测效率的提高以及远程医学的基本需求有着极大的意义。
|
| 关 键 词： | 概率模型检测 WBANs 攻击率 云辅助的轻量级无证书认证协议 PRISM |
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. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model[J]. Computer Science, 2019, 46(8): 206-211 |
| |
| Authors: | XIA Nu-nu YANG Jin-ji ZHAO Gan-sen MO Xiao-shan |
| |
| Affiliation: | (School of Computing,South China Normal University,Guangzhou 510631,China) |
| |
| Abstract: | XIA Nu-nu;YANG Jin-ji;ZHAO Gan-sen;MO Xiao-shan(School of Computing,South China Normal University,Guangzhou 510631,China) |
| |
| Keywords: | Probabilistic model checking Wireless body area networks Attack rate Cloud-aided lightweight certificateless authentication protocol PRISM |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
