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

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