孟博,唐获野,陈双.基于符号模型自动分析隐私保留的用户认证协议安全性[J].中南民族大学学报自然科学版,2019,38(1):138-143
基于符号模型自动分析隐私保留的用户认证协议安全性
Automatic analysis of security of privacy preserving user authentication protocol based on the symbolic model
  
DOI:10.12130/znmdzk.20190124
中文关键词: 大数据  用户认证  安全协议  形式化方法
英文关键词: big data  user authentication  security protocol  formal method
基金项目:湖北省自然科学基金资助项目(2018ADC150);中南民族大学中央高校基本科研业务费专项资金资助项目(CZZ18003,QSZ17007)
作者单位
孟博,唐获野*,陈双 中南民族大学 计算机科学学院武汉 430074 
摘要点击次数: 336
全文下载次数: 186
中文摘要:
      利用大数据特征,PPMUAS协议声称实现了移动用户的隐私保护和认证,但并没有给出严格证明.故本文首先应用Applied PI演算对PPMUAS协议进行形式化描述,然后分别使用非单射性和Query 对认证性和秘密性进行建模,最后把PPMUAS协议的Applied PI 演算模型转换为安全协议分析工具 ProVerif 的输入,应用ProVerif对其进行形式化分析与证明. 结果表明PPMUAS协议具有秘密性,但缺少认证性,并给出了解决方法.
英文摘要:
      Using big data features, PPMUAS authentication protocol claims to achieve user privacy preserving and authentication for mobile users, but it does not be proved by formal method. Hence in this study, firstly PPMUAS was formalized with Applied PI calculus. And then the secrecy and the authentication were modeled by Query and by non-injective correspondence respectively.Finally the Applied PI calculus model of the PPMUAS protocol was transformed into the input of the security protocol analysis tool ProVerif, was formally analyzed and proved through ProVerif. The results indicate that PPMUAS protocol has the secrecy, but has not authentication. At the same time the solutions for the problems were presented.
查看全文   查看/发表评论  下载PDF阅读器
关闭