一种支持三方认证的轻量级RFID双向认证协议

吴恺凡，殷新春，2

1(扬州大学 信息工程学院，江苏 扬州225127)

2(扬州大学 广陵学院，江苏 扬州 225128)

E-mail：xcyin@yzu.edu.cn

1 引 言

随着物联网概念的普及，万物互联的理念深入人心，为了满足不同行业内不同的具体需求，车联网、集装箱联网、畜联网等物联网系统应运而生[1-4].例如，车联网要求可信中心根据路边单元搜集到的数据实时追踪车辆，集装箱联网需要额外记录当前运输批次所有箱内的货物，畜联网需要对接牲畜下家以实现不同副产品的溯源等.而现有物联网无法满足不同应用场景各自的需求.除了对物联网本身的需求不足以及产品技术落后、管理平台研发缓慢、大数据缺乏合理管理等问题以外，物联网中交互数据以及用户隐私信息的安全问题同样成为限制物联网发展的原因.

射频识别(Radio Frequency Identification， RFID)技术被认为是21世纪最具发展潜力的信息技术之一.RFID电子标签不仅能为所附物体提供通信、计算的能力，同时也为通信和存储中的数据面临的安全问题提供了一个良好的解决平台.近年来，由于RFID能够降低成本、节省时间、减少所投入的人力资源，并提高生产力.因此，RFID的应用场景也越发广泛，从最初的物流、库存管理等，逐步扩展到监控、医疗、食品安全、供应链管理等多个领域.RFID系统由阅读器和标签组成，其中标签作为系统核心[5]，为系统提供了存储附着对象识别信息的低成本实现方式[6].

RFID的使用实现了物联网的智能化检测和身份识别.但是，标签与阅读器在公共信道通信的过程中，RFID系统经常会面临多种安全问题，比如隐私被泄露、数据被窃取等.造成这些问题的原因在于非法用户能够通过无线信道对系统执行多种类型的攻击，如主动攻击、被动攻击和物理攻击[7].主动和被动攻击的可行性建立在RFID电子标签和阅读器通过无线链路这一公共信道交换数据这一事实之上.开放环境下的通信使得所交换的数据完全暴露给公网内的所有用户，这使得RFID系统遭受攻击的风险陡增.再加上攻击者能够通过物理攻击监听相关设备在正常工作中的一些状态参数，这同样对RFID系统用户的隐私保护带来了不小的挑战.

为了解决RFID系统在无线通信安全上存在的问题和挑战，即提升系统的安全性、效率并加强隐私保护，不断有新的RFID认证协议被提出.但由于超轻量级协议大多无法满足安全需求，而诸如椭圆曲线加密算法(Elliptic Curve Cryptography， ECC)等复杂算法不易实现[8]，且会产生大量的时间开销和通信开销，不适用于低成本标签及RFID系统[9].因此，设计一个轻量级RFID认证协议迫在眉睫.本文的主要贡献如下：

1)针对标签匿名性不足的问题，我们提出了一种新的随机运算方法，并基于此方法设计出了一个能够保护标签所有者隐私的RFID双向认证协议.该协议配合二次剩余难题保护标签假名，除了能够保证匿名性以外，还能够满足物联网中RFID系统的安全需求；

2)我们使用BAN逻辑语言证明提出方案的安全性，使用AVISPA工具对提出方案进行仿真，并补充验证BAN逻辑不能证明的抗重放攻击和抗中间人攻击的安全属性；与相关认证方案进行性能方面的对比，结果显示，本文所提方案的计算时间复杂度和通信开销远优于能够提供同等安全性的非轻量级协议.

2 相关工作

20世纪以来，新的RFID身份认证协议相继被提出.这些RFID认证协议大体可以分成3类[10]：

1)只涉及位/比特运算或循环冗余校验(如CRC-16)的超轻量级认证协议[10-12]；

2)基于Hash、物理不可克隆函数(Physical Unclonable Function， PUF)或者伪随机数发生器(Pseudorandom Number Generator， PRNG)等单向函数的轻量级认证协议[13-17]；

3)运用非对称以及对称加密算法中一种或两种非轻量级认证协议[18-21].

以上3类的身份认证协议虽然都是通过协议双方互相通信来实现的，但从本质上来说仍然属于非交互式的证明系统，即传统数学证明系统.协议的某一方(在此称作己方)为了向对方证明自身具有合法身份，将明文形式的求证问题和密文形式的论据全部发送给对方.论据一般是密文形式的合法身份.己方发送求证问题请求对方提供论据.而对方收到求证问题后，能利用自身已知参数对该求证问题进行完整性验证，即已有参数涵盖了证明该问题所需的论据，至此对方主体成功证明己方主体身份合法.但是，这就依赖协议双方共享的秘密信息完成认证，且其安全性和计算资源使用效率需要通过通信认证协议、硬件设计以及密钥更新方式来衡量.从这些方面同样也能发觉某些方案的不足.例如，Aghili等人[12]提出了一种新型的超轻量级RFID认证协议SecLAP.SecLAP所用的加密算法是Aghili等人在二进制字符串的奇偶分离、取反、异或以及移位等比特运算的基础上设计出的模块化旋转函数.虽然作者声称SecLAP无明显的安全隐患，但是Safkhani等人[22]指出SecLAP容易遭受追踪攻击与秘密泄露.Gope等人[15]提出一种基于k-匿名和PUF以及Hash的轻量级RFID认证协议.但梁伟等人[23]指出文献[15]提出的方案由于设定不足，导致无法实现对假名列表中已消耗假名PID的补充，甚至攻击者可以通过重放攻击重放唯一身份标识TID以耗尽PID，迫使标签重新注册，从而阻断协议进程，增加标签的计算开销.Doss等人[16]提出了一种基于二次剩余并无安全信道的三方通信认证方案.文献[17]指出文献[16]提出的方案很容易受到重放攻击并提出了改进协议，但改进协议中的密钥无法更新且将当前认证周期开始的时间直接以明文发送作为时间戳认证，所以不能抵抗克隆攻击，会造成标签身份泄露.Rostampour等人[19]根据Diffie-Hellman密钥协商算法，提出一种基于ECC的RFID认证协议.但是由于私钥无法更新，所以该方案容易遭受克隆攻击、侧信道攻击等物理强主动型敌手的攻击.

然而，上述基于传统数学证明系统的RFID认证协议不能满足物联网发展需要.这是因为这一类协议要求各方遵守协议，以共同维护主体的身份安全.为了满足安全需求，协议会使得RFID系统数据库，即服务器方能够知晓标签所有的身份信息，包括ID、密钥、假名等，以实现恶意行为判别、溯源以及监管.但是，后端数据一旦发生泄露，或者不诚实的主体混入协议参与方，就会给攻击者假冒合法标签身份、欺骗合法用户、谋取非法利益提供便利.所以，相关研究者转而重点研究另一种证明系统，即交互式证明系统.交互式证明系统相较于传统数学证明系统，本身用做身份证明的信息无须完备，可通过多次提交不同的相关信息进行证明.当证明次数达到一定规模，且证明成功率达到一定标准时，可以近似认为该论点成立.假设在身份认证的场景下，那么传统数学证明系统中，证明者一次性将密文形式的合法身份发送给验证者，验证者解密后对比身份信息，这样在一次交互后就能得出验证结论；而交互式证明系统中，论据同样经过证明者加密后发送给验证者，并一定携带冗余信息，再由验证者以抛硬币的方式告知证明者是否需要将合法身份混淆进论据中，只有经过多次交互才能得出较为准确的验证结论.交互式证明系统的目的在于，Alice请求Bob验证自身身份.而Alice的钥匙则为Alice与Bob共享的密钥.在非交互式证明系统中，若身份认证协议是安全的，则认证性完全满足，而协议的安全性在于共享密钥在通信中以及存储时的机密性.而在交互式证明系统中，因为无需在公共信道传输密钥，即该系统只存在私钥，所以安全性一般高于非交互式证明系统，其认证性主要与验证次数正相关.这就是交互式证明系统用于身份认证的最大优势，即除了作为证明者Alice以外的所有主体都不知道Alice的身份信息，Bob却能够证明Alice是合法的.而交互式证明方式演变成了最初的零知识证明，即一方称为证明者，另一方称为验证者，证明者试图使验证者相信某个论断是正确的，却又不向验证者泄露任何有用的信息.为了实现这类交互式的零知识证明，Alice与Bob交互时同样需要满足3个条件：

1)冗余性约束：Alice需要用冗余信息来保护自身身份信息不被其他人获知；

2)针对性约束：Alice必须向Bob传递与自身身份信息相关的密文；

3)同源性约束：冗余信息的加密方式与Alice身份信息一致.

基于交互式零知识证明的RFID认证协议在执行过程中，仅仅向拥有验证权力的主体公布关于被验证主体拥有合法身份的证明论据，所有人对被验证主体的身份信息均一无所知，从而保证被验证者的合法身份被认证，又不会泄露其身份信息.这样，主体的身份安全就规约到了其自身的信息安全，而无需依赖协议中的其他主体为其保密.王坤等人提出了一种物联网环境下基于零知识证明的RFID双向认证协议.但是，零知识证明用于身份认证时，某主体身份的认证性若要通过对方验证，必须经历过多次验证.这又与RFID场景下，低成本标签计算资源有限这一现实相悖，所以该方案不适用于低成本环境.并且该方案中标签的身份信息不支持更新，所以也不能抵抗标签克隆攻击和追踪攻击.

为了弥补上述各方案的不足，提高RFID系统的适用性，并在低成本运行环境下保证各项安全需求，本文使用了一种原创的随机运算方法，结合二次剩余提出了一种RFID认证协议，该协议基于传统数学证明系统设计，称作RLMP3(Lightweight Mutual authentication Protocol between Three communication agents based on Random operators).

3 新型RFID匿名双向认证协议

在本文提出的协议RLMP3中，为了适应更加严苛的场景，扩大其适用范围，我们假设服务器与阅读器、阅读器与标签之间的通信信道都是不安全的公共信道.这就要求各个协议主体之间互相进行身份认证.

3.1 符号说明

RLMP3所使用的符号、函数，以及对应参数如表1所示.其中，洗牌函数Shuffle()过程如算法1所示.

表1 相关符号表Table 1 Symbols and cryptographic function

算法1.Shuffle(Seed,a)输入:Seed,a输出:a1.n←lengthofLista2.fori←0ton-1do3.4.j←randomintegerwithi≤j

3.2 协议认证过程

在本协议中，中央服务器和各个需要参与认证的标签都配有一个长度设为m的运算符表AT以存放具体的运算符，即服务器所服务的标签能够执行的各类轻量级运算及其可逆组合.在每轮认证周期中，互相通信的服务器和标签都共同遵循一个独立于不同标签个体的运算符选取顺序ST，根据其中存放的索引对应到各自的AT中寻找并存储运算符.但是阅读器对AT和ST一无所知.

Shuffle()算法的目的是将原数组随机打乱后生成新数组.本文所用的Knuth-Durstenfeld Shuffle算法[24]的具体做法是只执行一轮n次循环，每次循环将原数组的第i个数与第rand(i，n)个数交换，循环变量i的初值设为1，每次递增1直至原数组的长度n.该算法实现了原数组的原地洗牌，时间复杂度为O(n)，空间复杂度为O(1).

Shuffle()的功能是将长度为n的列表的第i个元素与第rand(i，n)个元素交换顺序，重复n次.只要在此基础上指定协议双方同一轮认证PRNG的种子，Shuffle()就能实现低成本环境下服务器和电子标签同步生成随机数.其中，Shuffle()的第1参数为PRNG的种子，第2参数为待处理列表，空参默认为一个依次存入正整数的列表.Shuffle()在协议中的作用是使得服务器和标签在每轮认证中同步按照一个随机的顺序选取AT中的运算符参与对会话密钥tk的混淆.

下面举一个Shuffle()的具体示例(随机假设一个AT，并且各个函数取一个可能的结果)，如图1所示.

图1 RLMP3自定义函数功能示例图Fig.1 Example of custom function in RLMP3

在紧接着的认证过程中，协议双方根据运算符索引表ST以及句柄参数j在运算符表AT中选取本轮参与计算的运算符.在确定运算符的过程中，句柄j的值作为ST的索引，ST[j]的值作为AT的索引.即?j=AT[ST[j(modm)]].在上述示例中，当前认证周期的第1个随机选出的运算符?1是循环右移(>>)，第2个?2是异或(⊕)，第3个?3是二分拼接(‖)，以此类推.由于标签选取的运算符最终只由PRNG的种子决定，因此可以说由PRNG对标签在当前轮次协议下的运算符选取序列完全负责.当j>m时，协议双方同时重置j，即计算j=j(modm).

协议的整个认证过程可以分为2个阶段，按照执行时序分为注册阶段和认证阶段.注册阶段是在第一次参与通信的标签参与协议时，由服务器和标签双方在安全信道中执行的，其目的是进行标签初始密钥的生成以及标签信息在服务器端的注册.每当标签与阅读器需要通信时，双方都会在通信前执行认证阶段.RLMP3协议的主要运算与数据传输如图2所示.

图2 RLMP3协议流程图Fig.2 RLMP3 process diagram

本协议在注册阶段中使用PUF，将自身的唯一身份标识TID作为挑战输入PUF去构造自己的初始会话密钥tk.此外，每个标签还会使用PUF，来构造针对不同标签的激励响应对(challenge and response pairs， CRPs)，或称挑战响应对，并将其作为第一轮的基础密钥组存储在服务器与对应标签之中，参与会话密钥tk的更新.服务器会将不同标签在注册阶段反馈的PUF响应Ri整合成一个基本密钥矩阵rij，其中横坐标i为标签序号，即行向量ri，*代表每个标签的基本密钥数组，经过注册后初始化为ri，*=Ri，而纵坐标j则为句柄序号，以表示标签i下一轮认证选用的基本密钥ri，j，选用范围仅限自身的基本密钥数组ri，*.

1.作为协议执行的先决条件，为标签提供服务之前的步骤定义为初始化阶段，该阶段中服务器会通过安全信道为每个已注册的阅读器分配一个假名rk，不同的阅读器假名也不同，同时服务器备份每个合法阅读器的唯一身份标识RID以及假名rk.需要注意的是，为了实现异步通信，即防止出现下述情况——当同一个阅读器同时参与多个标签的通信时，某一标签的认证引发阅读器假名更新会引起别的标签认证中发生去同步情况，服务器需要仿照操作系统中内核机制，做到以下两点：1)在某一标签引发认证周期后，别的标签认证中不能引发阅读器假名的更新，即给占用中的阅读器假名套上异步锁；2)根据等待时间动态更新不同标签的优先级，以一个合理的方式决定不同标签的认证顺序.

2.协议首先进入注册阶段，服务器端生成新鲜随机数组Ci，再将Ci发送给标签i.接收到Ci后，标签i将其作为PUF的挑战，对应生成响应数组Ri.此外，标签i还将自身的唯一身份标识TIDi作为PUF的参数，对应生成用作初始会话密钥的响应tki.然后，标签i将Ri，tki和TIDi一并发送给服务器.接着，服务器和标签将共同(共同指服务器在收到标签响应后执行，而标签在发送响应后执行下述计算)计算Seed=tki，即tki作为实现Shuffle算法的种子，最后计算STi=Shuffle(Seed)，即通过Shuffle()功能得到相同的STi.Shuffle()功能基于Shuffle算法，旨在给定协议双方相同的种子Seed，使得协议双方生成相同的ST，从而能够在之后的认证阶段实现秘密值的同步更新.

3.通信前首先由阅读器主动发起认证阶段.阅读器首先向标签发送一个询问信息，定义为“Query”，以开始新一轮认证周期.

4.在接收到询问信息后，标签i计算y=tki?jri，j，接着计算b=y2modn.其中，索引j对应指针，从0开始取值并在每轮认证周期的最后顺次递增.然后，标签i将参数b和假名tki发送给阅读器.

5.阅读器在收到标签回应后计算x=rk⊕tki，即通过将阅读器自己的假名以及标签发来充当会话密钥的标签假名异或生成二次剩余秘密值x，再以x为解计算a=x2modn，即模n的二次剩余a，最后将参数a和b发送给服务器.

7.识别标签与阅读器成功后，服务器计算验证参数VP1=PRNG(x)，VP2=PRNG(y)⊕PRNG(x+1)，并发送给阅读器，再更新标签假名tki←tki?j+1ri，j、阅读器假名rk←rk2modn、基础密钥ri，j←ri，j?j+2y、当前指针j←j+1，以及Seed←h(Seed‖y)，最后更新STi=Shuffle(Seed).

8.阅读器在收到验证信息VP1后进行验证，若VP1=PRNG(x)成立，则服务器的身份通过了阅读器的验证，随即更新其假名rk←rk2modn，计算并向标签i发送验证参数VP=VP2⊕PRNG(x+1)；否则意味着存在数据遭到攻击、篡改而阻碍了协议进程或是服务器本身身份非法等情况，认证失败，阅读器认为该服务器身份非法，通信过程终止.

9.标签i在接收到验证信息VP后展开验证，若VP=PRNG(y)不成立，意味着存在数据遭到攻击、篡改而阻碍了协议进程或是服务器本身身份非法等情况，认证失败，阅读器认为该服务器身份非法，通信过程终止；否则服务器的身份通过了标签i的验证，协议认证成功，标签为与服务器保持一致以便下次认证而更新以下信息：

4 非形式化安全性分析

在本节中，我们将从理论上分析所提出的RLMP3协议的安全性，证明其能够满足各项安全需求.

4.1 抗跟踪攻击

RLMP3实现标签的识别是从标签注册开始的.标签生成假名是通过PUF这一单向不可预测函数计算得到的.随后标签使用安全信道与服务器共享TID和tk.但是，标签发送TID只有在标签第一次注册并接入系统时才会发生，之后该标签在与此RFID系统内的服务器通信时，会用上一轮通信后更新的自身假名tk来表明自己的身份.所以，攻击者无法通过物理攻击以外的方式获取每个标签的唯一身份标识TID.并且在协议的每轮认证中，令牌tk都会进行动态的更新.当前标签下轮认证周期选用的随机运算符会跟随ST每轮动态更新而发生改变.而初始的基本密钥r会随着每一轮认证动态更新，设密钥数组R的长度为k，则该标签执行k轮认证后，R中所有元素都被更新过一轮.所以攻击者无法获取当前认证标签的TID，也无法将该标签的连续两轮认证中的tk相关联.因此，RLMP3能够有效抵御追踪攻击且标签匿名性也得到有效保证.

4.2 抗克隆攻击

攻击者在能获取合法标签的前提下仿制该标签，并在仿制芯片流片时烧录原合法标签的数据，最后取代原合法标签的身份.而参与RLMP3认证的标签使用PUF生成相关秘密值.这使得对应秘密值不可预测并且无法篡改，PUF本身无法被物理复制.攻击者只能通过克隆攻击获得某个合法标签的唯一身份标识TID.因此，RLMP3能够有效抵御标签克隆攻击.

4.3 抗伪造攻击

4.3.1 抗伪造标签

攻击者自己随机生成一个tk′伪装成合法标签来与阅读器交互.但是tk′很难与tk碰撞成功，若是攻击者使用已投入使用的或者自制的设备参与注册成为一个新的合法标签，则首先其唯一身份标识TID能够区分所有合法标签，其次注册阶段中PUF执行基础密钥r的初始化，所以不同标签的基础密钥r也不会发生碰撞.所以攻击者提取秘密响应r的概率相较于一般用户来说没有优势.

此外，攻击者无法从合法标签发送的消息中分离出随机运算符顺序表ST，并且无法保持与合法标签同步更新令牌tk.假设攻击者成功侵入协议的初始化阶段，从而获取了某个合法标签的有效身份信息tk，但是和标签的每轮认证周期很短，单次通信时间属于毫秒级操作，同时也难以通过若干次更新后的tk定位标签，所以攻击者难以定位与捕捉该合法标签.因此，RLMP3能够抵御标签伪造攻击.

4.3.2 抗伪造阅读器

攻击者通过随机生成一个自身假名去伪装成合法阅读器来与某一标签交互，因此攻击者可以获知当前认证周期的标签假名tk.但是其构造的消息和合法阅读器生成的x不同，所以无法通过服务器的验证.同样，相同阅读器的假名rk在进入下一个认证周期也支持更新，所以无法被攻击者用于当前周期内的伪造攻击.因此，RLMP3能够抵御阅读器伪造攻击.

4.3.3 抗伪造服务器

攻击者可以在协议过程中在公共信道截获模数n和余数a.但是大整数分解问题是近似NP问题，攻击者无法算出合数n的两个大素数因子p和q，所以无法通过中国剩余定理算出x.因此，RLMP3能够抵御服务器伪造攻击.

4.4 抗去同步攻击

攻击者通过破坏阅读器与标签之间在非安全信道上传输的某些消息的一致性，使得协议双方信息失去同步，从而阻碍正常的认证.攻击者实现去同步攻击主要有两种方式，一种是截获并篡改原有信息再发送给标签，另一种是截获原有信息并立即重新发送给标签，阻止对方的信息更新，以中断认证过程.攻击者甚至会大量发送这些信息，通过分布式拒绝服务(Distributed Denial of Service， DDoS)攻击的形式来达成这一目的.在RLMP3中，服务器端与标签都会额外存储上一轮的认证令牌tkold.当遭受去同步攻击导致服务器端与标签信息不一致时，认证双方中作为验证者的那一方会先用当前轮次认证令牌tknew进行验证，若匹配失败则再用上一轮成功通信的秘密值tkold进行对照匹配，匹配成功就能通过验证，使得认证流程继续进行并触发更新.因此，BRO-LAMP能够抵御去同步攻击.

4.5 抗重放攻击

攻击者成功捕获合法标签的身份验证信息，并请求使用这段信息进行身份验证，以欺骗合法标签或服务器.这种类型的攻击适用于不及时更新密钥的协议.另外，前后向安全性要求攻击者无法通过当前轮次认证的正确认证来推导出之前以及之后轮次的秘密信息.所提出的协议每轮认证中的每一次信息交互后，每轮认证的新鲜值ri，j、标签假名tk、阅读器假名rk以及随机运算表ST也经过更新或是重新生成.即不同轮次的秘密值均不同且不可预测，所以攻击者截获之前轮次的交互信息用于当前轮次认证的重放攻击均不会成功，符合前向安全性的要求.而随机运算表ST的更新意味着之前所使用的运算符与之后选取的没有逻辑关联，是随机不可预测的，符合后向安全性的要求.因此，RLMP3能够抵御重放攻击，同时保证了前后向安全性.

4.6 抗中间人攻击

攻击者通过拦截正常的网络通信数据，并进行数据篡改和嗅探来发动中间人攻击，而通信的双方却无法获知.所提出的协议在认证阶段的每一轮信息交互后，协议双方都会同步更新令牌tk以及更新所使用的运算符，当攻击者发动中间人攻击后，双方都能察觉到，所以篡改后的信息不会通过对方的验证.

5 形式化安全性分析

在本节中，在DY(Dolev-Yao)模型[25]下通过形式化分析的手段，分析所提出的RLMP3协议的正确性与安全性，证明其能够保证通信安全，并能够抵抗重放和中间人攻击.

DY模型中攻击者A可以拦截任何通信实体(在我们协议中是S、R和T)之间的消息，还可以修改、阻截消息或插入伪造的消息[26].本节对攻击者的能力设定也符合DY模型下敌手的定义.

5.1 BAN逻辑分析

BAN(Burrows， Abadi and Needham)逻辑[27]是一种基于信念的模态逻辑，并且是首个将形式化手段用于密码协议安全验证的分析法，因具有里程碑意义而被广泛应用.

BAN逻辑的具体符号表述如表2所示，P和Q代表参与协议的两个主体，X代表信息，K代表加密密钥.当信息以明文形式发送时，若是单个信息X，则表示为X，若是信息X与信息Y的复合信息，则表示为(X，Y)；当信息以密文形式发送时，则发送的信息X表示为{X}，若有下标，则表示用于加密信息X的密钥或是保证信息X机密性的秘密值.

表2 BAN符号Table 2 BAN symbols

BAN逻辑规则遵循推理规则的形式，即分为上、下两个部分，横线上方的公式集合称为前提，下方的公式则称为结论.在执行BAN逻辑分析时，必须严格遵循如下所示的特定公理.

根据相应公理、待验证协议的安全假设以及流程，如果BAN逻辑能够推演出该协议的安全目标，则说明该协议被证明足够安全.

RLMP3在BAN逻辑下的协议描述如下所示.

1)R→T：Query；

2)T→R：b，tk；

3)R→S：a，b；

4)S→R：h(x)，h(y)⊕h(x+1)；

5)R→T：h(y).

RLMP3的协议描述进一步修改成适合BAN逻辑证明的理想化模型后如下所示.

1)S1：T◁Query；

2)S2：R◁M2；

3)S3：S◁M4；

4)S4：R◁M7；

5)S5：T◁M6.

其中，S、R和T分别表示作为协议主体的服务器、阅读器以及标签.以下是协议描述中传递消息的详细描述.

1)M1=F(nonce，tk)；

2)M2=({M1}q，tk)；

3)M3=F(tk，rk)；

4)M4=({M1}q，{M3}p)；

5)M5=h(rk)；

6)M6=h(nonce)；

7)M7=(M5，F(h(rk+1)，M6)).

RLMP3协议的安全假设如下.

1)H1：T|≡#nonce；

2)H2：R|≡#rk；

3)H3：S|≡#nonce；

4)H4：S|≡#rk；

7)H7：S|≡T⟹M1；

8)H8：S|≡R⟹M3；

9)H9：T|≡S⟹M6；

10)H10：R|≡S⟹M5；

RLMP3协议的最终目标：

1)G1：S|≡M4；

2)G2：T|≡M6；

3)G3：R|≡M5.

根据上述初始条件，用BAN逻辑可证明RLMP3协议安全.

证明：根据模型步骤S3，分别结合假设H5和H6，由接收公理R5-1可分别推得：

S◁M1

(1)

S◁M3

(2)

结合公式(1)以及假设H5，根据消息意义公理R1可推得：

S|≡T～M1

(3)

同理，结合公式(2)以及假设H6，根据消息意义公理R1能够得出：

S|≡R～M3

(4)

接着，根据假设H3和新鲜性传递公理R4可推断出：

S|≡#M1

(5)

根据公式(5)可知消息M1是新鲜的，再结合公式(3)就能凑齐乱数证明公理R2的条件，从而得出：

S|≡T|≡M1

(6)

因为假设H7成立，所以S相信T拥有M1，结合上述公式(6)，根据管辖权公理R3而得到：

S|≡M1

(7)

同理，根据假设H4和新鲜性传递公理R4可推断出：

S|≡#M3

(8)

根据公式(5)可知消息M3是新鲜的，再结合公式(4)就能凑齐乱数证明公理R2的条件，从而得出：

S|≡R|≡M3

(9)

因为假设H7成立，所以S相信R拥有M3，结合上述公式(9)，根据管辖权公理R3而得到：

S|≡M3

(10)

综合公式(7)和公式(10)就能证得：

S|≡M4

(11)

至此目标G1得证，这也意味着服务器成功通过随机值nonce和阅读器假名rk分别证明标签和服务器的身份合法.

需要注意的是，标签通过服务器的身份认证必然早于阅读器，因为服务器只有通过单向可逆函数F的逆函数F-1才能将消息M1中的标签假名tk和随机值nonce分离，从而在使用新鲜的tk认证标签身份的同时将消息M3中的rk与tk分离，以保证接下来对阅读器的身份认证.

根据模型步骤S4以及接收公理R5-2得：

R◁M5

(12)

由上述公式(12)以及假设H11，根据消息意义公理R1可得：

R|≡S|～M5

(13)

假设H2和新鲜值传递公理R4可得出结论R|≡#M5，配合公式(13)，再根据乱数证明公理R2可得出：

R|≡S|≡M5

(14)

根据上述公式(14)与假设H10，就能通过管辖权公理R3证得：

R|≡M5

(15)

至此，目标G2证毕，阅读器证明服务器合法，之后阅读器配合服务器更新假名rk用于下次与服务器的双向认证.

根据模型步骤S5，标签T收到h(nonce)再加上假设H12，根据消息意义公理R1可得：

T|≡S～M6

(16)

已知假设H1和公式(13)，根据乱数证明公理R2可得出：

T|≡S|≡M6

(17)

根据上述公式(17)与假设H9，就能通过管辖权公理R3证得：

T|≡M6

(18)

至此，目标G3证毕，标签证明服务器合法，之后标签配合服务器更新假名tk用于下次与服务器的双向认证.

综合公式(11)、公式(15)以及公式(18)，RLMP3协议的认证目标全部证毕，且协议安全.

5.2 AVISPA仿真

BAN逻辑有如下缺点：

1)BAN逻辑只讨论对诚实主体的认证性，即无法限定哪些主体不能获取相关秘密值；

2)BAN逻辑的安全性与方案的步骤无关，即协议执行顺序打乱导致的安全性问题会漏检.

AVISPA是一款高效、稳定的，广泛适用于自动证明网络安全协议、应用以及能够反映实际工业环境复杂度的威胁模型的安全性的工具集，能够根据相应规则推导安全性目标[28，29].此外，AVISPA还能评判协议是否能够免受重放和中间人攻击[30].作为一个实用的形式化验证工具，AVISPA包含4种模型检测后端.我们通过高级协议规范语言(High Level Protocol Specification Language， HLPSL)对RLMP3协议进行仿真，并使用4种后端中的前2种，即时模型检验器(On-the-fly Model Checker， OFMC)以及基于约束逻辑的攻击搜索器(Constraint Logic-based Attack Searcher， CL-AtSe)进行检测.

二次剩余问题在数学领域是困难的，可用作密码学算法与协议设计[31].假设p是模n的二次剩余，且p、n互素，那么二次剩余问题的解决难度主要在于，大合数模n虽然被公开，但不知道n所有素因子的主体无法在多项式时间内解出二次剩余方程x2≡pmodn，且难度等价于分解这个大整数n[32].由于HLPSL语言只支持异或和乘幂却并不支持加减乘除以及模运算，因此无法体现二次剩余这一NP问题的困难性.因此，使用HLPSL仿真RLMP3，需要用对称加密来代替二次剩余.协议中，模n的素因子p和q作为服务器S的私钥，而模n的二次剩余a和b则分别作为R和T发出的身份认证消息的密文.

AVISPA运行RLMP3的HLPSL描述代码后的结果如图3和图4所示.

图3 动态模型检测结果截图Fig.3 Screenshot of result tested by OFMC

图4 基于约束逻辑的攻击搜索器检测结果Fig.4 Screenshot of result tested by CL-AtSe

如果一个协议经过AVISPA仿真后检测到了安全漏洞，“SUMMARY”字段则会显示为“UNSAFE”，并在“DETAILS”字段提示“ATTACK_FOUND”，最后会在“GOAL”字段提示出该协议所需证明的安全属性中首先检测到的那一个没有满足的安全属性.分析过程中，由HLPSL描述的协议经编译后转换为中间形式(Intermediate Format， IF)保存在“PROTOCOL”字段给出的路径最后所示，文件名为“BRO-LAMP.if”的文件中.结果中的“BACKEND”字段显示了所用后端分析工具类型，“STATISTICS”字段则说明了分析工具所执行的时间及搜索的节点数或状态数量.从图3和图4的检测结果中，根据“SUMMARY”字段显示为“SAFE”且“GOAL”字段提示“as specified”，我们可以推断所提出的RLMP3协议能够抵抗各类主、被动攻击.

6 性能分析

6.1 安全性对比

本节通过RLMP3应对多种恶意攻击的抵御能力与所满足的安全属性，与其他RFID认证协议进行对比.RLMP3与相关方案安全性能比较如表3所示，“Yes”表示该列对应协议满足该行对应的安全属性或者能够抵抗该行提到的攻击，标注“No”则表示协议不支持该安全属性或无法抵挡该类型的攻击.

表3 安全性对比Table 3 Security comparisons with other protocols

根据表3可得，在与相关方案的安全性对比中，只有RLMP3协议能够满足所有提到的RFID系统需要满足的安全需求.RLMP3在保证无线通信安全的同时也能够抵抗克隆攻击.

6.2 性能对比

本节将从计算复杂度与时间效率两个方面将RLMP3协议与其他协议进行性能分析和对比，如表4-表6所示.表4统计了参与协议的不同主体(S、R、T分别代表服务器、阅读器以及标签)在认证过程中使用对应运算的次数.表5给出不同运算在一定硬件条件下的单次耗时数据，相应的时间单位为毫秒，其中基本运算的数据参考文献[30]得来，而缺失的模逆运算的耗时数据则通过文献[32]得到.并且根据文献[33]，我们将忽略时间开销远小于模幂、标量乘法等的轻量级运算的开销，例如异或与连接等.针对相关运算的程序模拟是在虚拟机上进行的，并且该虚拟机的配置为英特尔酷睿第一代i5-560M主频2.67GHz双核四线程CPU(Central Processing Unit， 中央处理器).综合表4和表5的结论，计算出不同方案的计算总耗时并在表6中给出，时间单位为毫秒.设存储交互的相关信息的长度为L.为了保证大整数分解的困难性，L以及作为秘密值的奇素数p和q取1024 bits.

表4 复杂度对比表Table 4 Complexity comparison

表6 实际耗时对比表Table 6 Real-time complexity comparison

综合表4-表6可得，在与相关方案的计算性能对比后，我们发现只有文献[17]的方案与RLMP3协议适用于资源受限的无源标签，并且能够高效计算.因为文献[20]和文献[21]的方案采用了相对复杂的ECC算法，其认证时加解密使用的标量乘计算量大，响应时间长.而文献[17]的方案虽然使用二次剩余，但标签需要存储相对更多的会话密钥，存储开销大.相较而言，RLMP3协议能在低成本环境表现出较好的性能.

7 结 语

本文提出了一种支持三方认证的RFID匿名协议RLMP3.该协议不再局限于“服务器与阅读器之间只能在安全信道工作”的传统系统模型，实现了阅读器与标签分别与服务器之间的匿名双向认证，适用于配备便携式阅读器的物联网场景.同时本文用非形式化和形式化的方法分析并证明了该协议的安全性.本文通过安全性和性能对比分析证明了RLMP3协议在安全性和计算性能方面都有较大的优势.协议中包含的新的随机运算符选取思想，能够使整个RFID系统可以抵抗主动、被动、物理攻击.并且该思想也能够应用于其他适用于物联网的身份认证协议的改进.