基于Java程序验证医疗系统RFID协议的抗跟踪能力

陈秀清 胡俊峰 马凯 耿德勤 袁洋 刘伟 朴雪 张红伟 朱婷婷 郝杰 徐州医科大学医学信息学院 （江苏 徐州 221008）

内容提要： 基于RFID系统在医疗应用中的作用以及在医疗体系中的关键角色，研究提出了基于移动医疗环境的RFID协议，采用Vaudenay模型对协议进行形式化分析。提出一种适用于移动医疗的基于Hash运算的RFID双向认证协议，基于JAVA程序证明了新协议具有强大的抗追踪能力。

基于RFID系统的应用在医院中发挥了不可替代的作用，如药品使用跟踪、医护人员定位、患者的管理等。无源电子标签在医疗单位的应用最为广泛，它可以极大地降低医疗辅助设施的成本，因此本文分析的协议都是针对无源的RFID标签。针对超轻量级协议的位篡改攻击形式可以从分析比特流开始[1]。SASI协议是超轻量级RFID认证协议，而文献提出了SASI协议存在去同步化攻击[2]。2013年，曹峥等使用串空间模型给出了去同步化攻击的判定定理，但是该定理通过引入攻击者串，找出针对具体协议的攻击方法[3,4]。Sun等重点分析了Ahmadian等提出的RAPP认证协议，揭示了该协议存在去同步化攻击[5]。很多研究从性能、安全性等级、可扩展性和串空间理论等多个方面深入分析协议存在的典型问题，随后提出改进措施和方法。最近提出的协议包括随机化Hash-Lock RFID认证协议[6]、Hash链协议[7]、ESAP协议[8]、SASI协议[9]、KMAP协议[10]。为了提高将来的移动医疗系统的标签验证效率和降低标签生产的成本，未来会借鉴协议的基于物理层（Physical-Layer）来提高标签识别效率，设计面向大范围移动医疗RFID系统[11]。

本文提出适用于医用环境中的低成本中量级RFID的协议，经模型证明新协议的有效性。并通过形式化以及程序仿真等方法，证明了新协议具有更好的抵抗跟踪攻击的能力。

1.基于Hash函数的RFID安全协议

本文基于Hash函数提出了HPAP协议，协议符号和定义见表1。

HPAP协议见表2交互过程如下：①服务器对标签和阅读器执行强认证机制，当阅读器和标签验证M2=M2ʹ。如果不成立，协议终止。②阅读器提供其秘密值和更新操作，抵抗阅读器假冒攻击，利用 fl ag机制表明密钥是否通过验证。

表1. HPAP协议符号和定义

表2. HPAP协议的执行流程

表3. HPAP协议标识符泄露下的跟踪测试

2.验证HPAP协议的跟踪攻击能力

本文对HPAP协议的仿真采用了Windows 7系统下基于eclipse.4.5.2+Java SE搭建的开发环境。HPAP协议测试数据在ID=10000，IDS=238495，Stnew=5463669，RID=2500，RIDS=468467，Sr=97535条件下，数据参数采用16进制。在医用环境中如果存在假冒阅读器的行为，那么敌手必须捕获阅读器的秘密信息Sr，对于Weak级别的敌手攻击协议成功的概率为0，所以该协议满足Weak隐私。见表2。

利用Java程序使用数值仿真的方法验证HPAP协议满足不可跟踪性。由于Hash函数单向特性，由IDSnew=H(Per(IDS,ID)⊕ΔS)，在多项式时间内，只要根据上一次的IDS推断出下一次交互的IDSnew即可认为HPAP协议的标签被跟踪。攻击形式分为两种：

测试数据的条件是ΔS=34455553，ID=5000，腐化攻击下的跟踪攻击测试结果如表3所示，测试次数为百万次。由HPAP协议使用随机数明文传递方式决定攻击测试采用了ΔS定值测试法。因此，表3中的数据可以代表该协议抵抗跟踪攻击情况，实验情况也反映了当标签标识符被捕获时，针对标签的跟踪攻击概率很小。Java程序测试了其他20条不同的记录，发现这些跟踪攻击普遍小于6%，并且每次跟踪攻击必须进行百万次的试探，反映了HPAP协议具有很强的抗追踪能力。

3.小结

本文提出了一种基于Hash函数的HPAP协议，使用形式化证明的方法证明了HPAP协议可以抵抗跟踪攻击，即具有强隐私程度；使用JAVA仿真软件对HPAP协议进行了仿真并对其抗跟踪能力进行Java程序测试，验证了HPAP协议具有较强的抗跟踪能力。