基于符号模型自动分析隐私保留的用户认证协议安全性

孟博，唐获野，陈双

(中南民族大学 计算机科学学院，武汉 430074)

随着大数据[1,2]及其应用的快速发展，应用大数据挖掘和分析[3,4]可以发现许多敏感信息，如：用户隐私信息、健康数据和医疗保健信息等，因此大数据安全和隐私[5-7]受到了人们的重点关注，研究重点是保留用户隐私的身份认证协议.

目前人们提出了许多面向大数据的用户身份认证协议[8-12].2012年，基于用户笔迹模式特征和用户口令，Omri等[8]提出安全地访问云；2013年，应用基于ID /密码、移动识别号码和用户生物信息，Jeong等[9]提出了移动云计算的多因素身份认证协议，实现了智能设备和服务器集群的相互认证并且提高了认证的性能；面向移动设备平台，Dey等[10]应用MDA(Message Digest Authentication)提出了一种身份认证协议，实现了移动设备和云服务器的相互认证；面向云计算环境，基于零知识认证、数字签名和模糊保险库，Schwab and Yang[11]提出了一种面向移动用户的FDZ认证协议，用于验证云计算环境中的移动设备.然而，这些工作没有重点关注用户隐私信息. 2016年，面向云环境，利用大数据特征，Vorugunti等[12]提出了一种隐私保护的多因素移动用户身份认证协议PPMUAS.据悉，它是第一个声称实现了用户身份认证和用户隐私保护的认证协议.Vorugunti声称该协议具有认证性和隐私性.但是，没有进行严格的分析和证明.应用形式化方法，自动分析和验证协议认证性[13,14]已被广泛使用.故此，基于符号模型，本文首先应用Applied PI 演算对PPMUAS身份认证协议进行形式化建模得到其形式化模型，然后分别使用非单射一致性和 Query 对认证性和秘密性进行建模；最后把PPMUAS身份认证协议的Applied PI 演算模型转换为安全协议分析工具 ProVerif[15]的输入，应用 ProVerif 对其进行形式化分析，结果表明PPMUAS身份认证协议具有秘密性，但不具有认证性，最后给出了实现认证性的方法.

1 PPMUAS认证协议的消息结构

PPMUAS协议包含3个实体：用户User，认证服务器As，数据库DB.其协议消息结构如图1所示，主要包含6条通信消息.

图1 PPMUAS协议的消息结构Fig.1 Protocol message structure of PPMUAS

1.1 用户注册请求

用户User注册时向认证服务器发送一条注册请求消息1 Registration request，该消息包含用户身份码Idi、 用户代号i、用户配置文件Cupi和Rpwi.Rpwi由哈希函数Hash对用户口令Pwi、随机数bi进行散列生成；Cupi由模糊哈希函数FuzzyHash和同态加密函数FH_Enc生成.模糊哈希函数FuzzyHash对Pwi，U_OlInfo和U_BrInfo进行散列，同态加密函数FH_Enc对U_KeySD，U_AMM和U_GM进行加密，最后把消息1发送给认证服务器.

其中U_OlInfo是用户在线信息、U_BrInfo是用户浏览器信息、U_KeySD是用户击键动力学信息、U_AMM是加速度计测量信息、U_GM是陀螺仪测量信息.

1.2 认证服务器注册请求

认证服务器接收到消息1 Registration request后，通过哈希函数Hash对Idi，Rpwi和i进行散列得到Vi并存储到认证服务器中；同时产生消息2 Authentication server request.该消息包含α，Rpupi和i.其中，α由随机数ri和用户特定秘钥kn通过公钥k1加密得到，Rpupi通过以下方法得到：首先通过置换函数Permute(P)重新排列用户加密文件Cupi得到Pupi，再将Pupi与ri进行异或运算(XOR)，最后生成消息2发送给数据库.数据库用k1解密得到ri和kn.Pupi由Rpupi和ri通过XOR计算得到，最后将ri，kn和Pupi保存到数据库，用户的注册完成.

1.3 用户登录请求

1.4 认证服务器登录请求

1.5 数据库响应

1.6 登录响应

认证服务器在收到消息6 Login response，首先检查消息参数，若是yes则允许用户接入服务，否则拒绝用户接入服务.

2 应用Applied PI演算对PPMUAS认证协议形式化建模

2.1 函数和等式理论

函数和等式理论主要包含：公钥算法包含加密算法aenc(x,Pu)和解密算法adec(y，Pu).aenc(x,Pu)对应用公钥Pu对消息x进行加密生成密文.adec(y,Pu)使用公钥Pu对消息y解密得到明文.异或算法XOR(x,y)对消息x，y进行异或计算.汉明重量算法HW(x,y)对消息x，y进行汉明重量测量.置换函数P对消息x进行置换.其形式化建模如下：

2.2 进程

完整的PPMUAS协议进程主要包含：用户进程processUser、认证服务器进程processAs和数据库进程processDB.它们共同构成了主进程，具体表述如下：

使用Applied PI演算对用户进程建模为processUser.

注册阶段，用户进程使用new语句生成用户的个人隐私信息.然后使用模糊哈希FuzzyHash和同态加密FH_Enc分别对参数进行计算，通过let in语句将生成的用户个人隐私文件赋值给Cupi，同时将用户输入口令Pwi与随机数bi进行哈希散列，散列值用let in语句赋值给Rpwi，最后通过公开信道c把注册消息e发送给认证服务器进程；

登录阶段，用户再次执行与注册阶段相同的工作，将登录消息e′发送给认证服务器进程.若登录成功则会通过信道c接受到认证服务器返回的登录响应.processUser具体表述如下：

let processUser=

new U_OlInfo

new U_BrInfo

new U_KeySD

new U_AMM

new U_GM

let Rpwi=Hash(Pwi,bi) in

let e=(IDi, Rpwi, Cupi,i) in

out(c,e)

new U_OlInfo′

new U_BrInfo′

new U_KeySD′

new U_AMM′

new U_GM′

let Rpwi=Hash(Pwi,bi) in

out(c, e′)

in(c,ticket)

使用Applied PI演算对认证服务器进程建模为processAs.

注册阶段，通过公开信道c收到消息m1，通过对Rpwi、用户Idi和用户代号i进行哈希运算得到散列值Vi并存储在认证服务器本地，同时用户个人隐私文件Cupi通过P运算得到Pupi，Pupi与随机数ri进行异或运算得到Rpupi，最后ri，kn与Pu(k1)做对称加密得到α，通过公开信道c将α，Rpupi和i一起发送给数据库；

let processAs=

in(c, m1)

new ri

new kn

let (IDi, Rpwi, Cupi,i)=m1in

let Vi=Hashone(IDi,Rpwi,i) in

let Pupi=P(Cupi) in

let Rpupi=XOR(Pupi,ri) in

let a=aenc((ri,kn),Pu(k1))in

let DB=(a,Rpupi,i) in

out(c, DB)

in(c, m3)

new yeah

new knn

out(c, DB′)

in(c, yes)

out(c, ticket)

使用Applied PI演算对数据库服务器进程建模为processDB.

注册阶段，通过公开信道c收到消息m2，通过对称解密adec(a,Pu(k1))得到ri和kn，然后异或运算得到Pupi，至此用户完成在数据库的注册.

let processDB=

in(c,m2)

let(a,Rpupi,i)=m2in

let(ri,kn)=adec(a,Pu(k1)) in

let Pupi=XOR(Rpupi,ri) in

in(c,m4)

let (ri,knn)=adec(a′,Pu(kn)) in

new yes

out(c, yes)

3 利用ProVerif验证PPMUAS认证协

议的秘密性和认证性

ProVerif应用非单射一致性来建模认证性，因此应用ev: event one→ev:event two来建模认证性.如果事件ev: event one被执行，那么事件ev:event two必定被执行.PPUMAS身份认证协议认证性建模如表1所示.同时，应用ProVerif中query attacker:Pwi验证用户口令Pwi的秘密性.

表1 认证模型Tab.1 Authentication model

ProVerif 的输入有 Horn 子句和Applied PI 演算两种方式，本文建模选择Applied PI 演算作为输入，Appied PI 演算输入必须转化为 ProVerif 的语法才能输入到 ProVerif 工具运行，图2为转化后的 ProVerif 输入及添加验证认证性的事件查询.

4 分析结果

应用ProVerif 运行PPMUAS协议的ProVerif格式的输入，结果如图3～图5所示.query attacker：Pwi运行结果如图3所示，其结果是true，证明用户口令Pwi具有秘密性.因为用户对口令Pwi进行哈希散列，得到的是口令摘要值，将摘要值发送给认证服务器,攻击者无法获得口令.

图3 Pwi秘密性Fig.3 Pwi secrecy

认证服务器对数据库的认证结果是“cannot be proved”，表明认证服务器不能实现对数据库的认证，因为数据库返回给认证服务器的消息Database response只有一个参数yes/no，并且消息没采取安全机制，故攻击者通过监控公开信道可以直接发起冒充攻击，因此，认证服务器不能认证数据库服务器.

图4 认证服务器与数据库相互认证结果Fig.4 Mutual authentication results between authentication server and database

图5(a)和(b)分别是认证服务器对用户认证性和用户对认证服务器认证性的建模分析结果，两者的结果均为“cannot be proved”，说明认证服务器和用户之间不能相互认证.因为用户对发送给认证服务器的消息3 Login request未作任何安全处理，攻击者可以监控公开信道，得到消息3的内容，进而发起冒充攻击，因此，不能实现认证服务器认证用户；并且认证服务器发送给用户的消息6 Login response中只包含一个参数ticket/reject，并且消息未作任何安全处理，攻击者通过监控公开信道得到消息，进而发起冒充攻击，因此不能实现用户认证认证服务器.

图5 认证服务器与用户相互认证结果Fig.5 Mutual authentication results between authentication server and user

5 结论

随着大数据挖掘和分析技术的发展，大数据安全和隐私受到了人们的重点关注，特别是保留用户隐私的身份认证协议已经成为一个非常活跃的研究领域.利用大数据特征，认证协议PPMUAS声称实现了移动用户的隐私保护和身份认证.但是本文通过对其使用基于符号模型的ProVerif进行形式化建模分析后发现，认证服务器对数据库具有认证性，而数据库对认证服务器无认证性，用户和认证服务器间均无认证，对于用户口令Pwi有秘密性.

关于认证服务器与用户的相互认证性和认证服务器对数据库的认证性，可以在不引入新的秘钥系统[16,17]下，分别对消息3 Login request，6 Login response和5 Database response中的参数进行数字签名[18,19]，从而实现认证性.

将来对PPMUAS协议进行改进，在完善认证性的基础上，通过隐私度量[20,21]对其隐私性进行量化分析.同时，通过引入差分隐私[22,23]改善其隐私性.