适用于无线体域网的动态口令认证协议

杜梦瑶，王 峥，李 娜，强 彦

1.太原理工大学 信息与计算机学院，山西 晋中 030600

2.国网山西省电力公司，太原 030024

1 引言

无线体域网（Wireless Body Area Network，WBAN）是指以人体为核心，由一系列嵌入式或者可穿戴传感器节点和个人智能设备（如智能手机、PDA等）组成的无线通信网络。个人服务器收集传感器获取的生理信息后，通过无线局域网传递至医疗服务端，由医疗服务端对患者的病情进行诊治[1]。由于无线网络的开放性，无线体域网在给人类带来医疗帮助的同时，存在的安全问题也日益突出。身份认证一方面可以防止非法用户登录服务端享受资源和服务，同时另一方面也可以防止攻击者假冒合法医疗服务端获取病人的敏感数据[2-3]。因此，无线体域网认证协议的安全性问题成为近几年来无线体域网领域研究的热点[4]。

现有的WBAN身份认证方案主要分为两类，基于人体生物信息的认证方案和基于传统密码学的认证方案[5]。朱淑文等人于2018年设计了用心电特征作为认证私钥的双向认证协议，实现了用户与医疗服务端的相互认证[6]，但心电特征较难进行提取。Dodangeh P等人于2018年设计了整个无线体域网网络架构的安全方案，使用生物识别技术作为认证和密钥交换的一部分，通过BAN逻辑验证方案能够抵御各种攻击[7]，但生物识别技术存在偶然性大、误差性大的问题。因此，总体来说，基于人体生物特征信息的身份认证方案存在生物信息难提取、较大偶然性和较大误差性的缺陷，所以这种身份认证方法有待进一步商榷[8]。陈少辉于2015年在无证书公钥密码体制的基础上提出一种新的基于无对的无证书签名认证协议，但该方案存在用户与服务器认证复杂、速度慢的缺陷[9]。Yeh H L等人于2011年在分析Das等人提出的无线体域网认证方案存在内部攻击和伪造攻击的基础上，提出一种基于ECC机制的认证协议[10]，但后被指出该协议不能有效完成双向认证[11]。文献[8]中，彭彦彬等人基于挑战应答S/Key，SAS和SAS-2认证协议低成本的优点，通过引入设备标志、减少哈希运算与消息传输次数等方法，提出一种端到端的医疗无线体域网认证方案，该方案经测试各项资源占用和能耗指标总体上小于挑战应答协议，但该协议不能抵御拒绝服务器攻击。

本文对前人提出的无线体域网认证协议的优缺点进行总结分析，针对人体生物信息的认证方法和传统密码学的认证方法不能满足无线体域网环境的问题，基于动态口令（又称一次性口令，Dynamic Password，DP）的轻量、随机性、动态性和一次性[12]及非对称加密算法的高安全性，提出一种适用于无线体域网的动态口令双向认证协议，并对协议采用SVO逻辑推理方法[13]和SPIN模型检测实验方法进行形式化验证分析。

2 WBAN_DPAP认证协议

本文提出的无线体域网的动态口令认证协议WBAN_DPAP（Wireless Body Area Network_Dynamic Password Authentication Protocol）分为两个阶段：协议注册阶段和协议认证阶段。注册阶段只在客户第一次登录医疗服务端时执行，认证阶段在每次登录医疗服务端时执行。协议由两个实体组成：个人服务器实体和医疗服务端实体。为了方便协议描述及形式化分析，表1给出协议过程中使用的具体符号定义。

表1 WBAN_DPAP协议符号定义表

2.1 WBAN_DPAP协议注册过程

WBAN_DPAP协议注册过程的步骤如下：

（1）PS实体向MS实体发送注册请求消息，执行msg1。

msg1：PS(注册请求)→MS

（2）MS实体收到消息后，执行msg2。

msg2：MS(KMR)→PS

（3）PS实体收到消息后保存KMR，并计算EKMR(PID//KPR//PW)，执行msg3。

msg3：PS(EKMR(PID//KPR//PW))→MS

（4）MS实体收到消息，用其私钥进行解密得到PID、KPR、PW并保存，同时产生随机数MR并保存为MR′。计算EKPR(MID//MR)，执行msg4。

msg4：MS(EKPR(MID//MR))→PS

（5）PS实体对msg4进行解密并保存MID、MR。

WBAN_DPAP认证协议的注册过程如图1所示。

图1 WBAN_DPAP协议注册过程

2.2 WBAN_DPAP协议认证过程

WBAN_DPAP协议认证过程的步骤如下：

（1）PS实体输入PID、PW，提取当前时间戳T1，产生随机数PR并保存为PR′。计算(EKMR(PID//H(MR//PW)//PR//T1)//T1)，执行Msg1。

Msg1：PS(EKMR(PID//H(MR//PW)//

（2）MS实体在T∗1时刻收到消息。若T∗1-T1≤ΔT，则接收认证请求，否则拒接登录认证。

（3）MS计算 DKMS(EKMR(PID//H(MR//PW)//PR//T1))，得到 PID、A=H(MR//PW)、PR、T1，首先检查解密得到的时间戳与未加密时间戳是否一致，若不一致，则认为认证失败。其次检查医疗服务端是否保存PID所对应的PW，若不存在，则认证失败，否则计算B=H(MR′//PW)。最后进行验证，若A=B，则PS为合法实体，若不相等，MS拒接其认证请求，认证结束。

（4）若PS为合法实体，MS提取当前时间戳T2，产生随机数MR并保存为MR′以供PS下次验证，计算 EKPR(MID//H(PW//PR)//MR//T2)//T2，执行Msg2。

Msg2：MS(EKPR(MID//H(PW//PR)//

（5）PS实体在T∗2时刻收到消息。若T∗2-T2≤ΔT，则接收认证请求，否则拒绝登录认证。

（6）PS计算 DKPS(EKPR(MID//H(PW//PR)//MR//T2))，得到 MID、C=H(PW//PR)、MR、T2，首先检查解密得到的时间戳与未加密时间戳是否一致，若不一致，则认证失败。其次计算D=H(PW//PR′)，最后进行验证，若C=D，则MS为合法实体，否则认证结束。

WLAN_DPAP认证协议的认证过程如图2所示。

图2 WBAN_DPAP协议认证过程

3 WBAN_DPAP协议安全性分析

3.1 基于SVO逻辑的WBAN_DPAP协议分析

1994年，Syverson P和van Oorschot P C提出SVO逻辑，其标志着BAN及BAN类逻辑的成熟[14]。SVO逻辑可以有效地发现协议设计中的漏洞和安全漏洞，并在认证协议的形式化分析中发挥重要作用。

SVO逻辑包含2个初始规则和20条公理，本文协议认证过程使用的包括必要性规则Nec、源关联公理Ax4、接受公理Ax7、Ax8、看见公理Ax10、说过公理Ax14、新鲜性公理Ax17、Nonce验证公理Ax19，具体如下：

必要性规则Nec：|-φ⇒|-P believes φ

Nec规则表明，如果φ是一个定理，则P believes φ也是一个定理。

源关联公理Ax4：

PKσ(Q,K)∧R received X∧SV(X,K,Y)⊃Q said Y

Ax4表明，如果R收到X，且签名验证通过，则可推理出Q说过Y。

接收公理Ax7：

P received(X1,X2,…,Xn)⊃ P received Xi

Ax7表明，主体接收到一个消息，也同时接收了该消息的连接项。

接收公理Ax8：

Ax8表明，如果主体拥有解密密钥，可以获得被加密前的消息。

看见公理Ax10：P received X⊃P sees X

Ax10表明，一个主体能看见所有它接收到的。

说过公理Ax14：

Ax14表明，一个主体只能说他所拥有的。

新鲜性公理Ax17：fresh(Xi)⊃fresh(X1,X2,…,Xn)Ax17表明，若 Xi是新鲜的，则其级联(X1,X2,…,Xn)是新鲜的。

Nonce验证公理Ax19：

Ax19表明，如果X是新鲜的，且主体说过X，就意味着主体最近说过，也即在当前时期内说过。

使用SVO逻辑对协议的形式化分析分为三个步骤，即给出协议初始化假设、列出协议目标和进行推理证明[15]。

（1）协议初始化假设

P1：PS believes fresh(PR)

P2：MS believes fresh(MR)

P3：PS believes PKσ(PS,KPS)

P4：MS believes PKσ(MS,KMS)

P5：PS believes PKψ(MS,KMR)

P6：MS believes PKψ(PS,KPR)

P7：PS received{MID,H(PW,PR),MR,T2}KPR,T2

P8：MS received{PID,H(MR,PW),PR,T1}KMR,T1

P9：PS believes SV({MID,H(PW,PR),MR,T2}KPR,KPS,{MID,H(PW,PR),MR,T2})

P10：MS believes SV({PID,H(MR,PW),PR,T1}KMR,KMS,{PID,H(MR,PW),PR,T1})

给出主体对接收到的消息的理解

P11：PS believes PS received{MID,H(PW,PR),MR,T2}KPR,T2

P12：MS believes MS received{PID,H(MR,PW),PR,T1}KMR,T1

（2）协议目标

T1：PS believes MS says H(PW,PR)

PS believes PS sees H(PW,PR)

T2：MS believes PS says H(MR,PW)

MS believes MS sees H(MR,PW)

（3）推理证明

根据P11，Ax7可得：

PS believes PS received{MID,H(PW,PR),

根据P12，Ax7可得：

MS believes MS received{PID,H(MR,PW),

根据式（1），P3，Ax8，Nec可得：

PS believes PS received{MID,H(PW,PR),MR,T2}（3）

根据式（2），P4，Ax8，Nec可得：

MS believes MS received{PID,H(MR,PW),PR,T1} （4）

根据式（3），Ax7可得：

PS received PS received H(PW,PR) （5）

根据式（4），Ax7可得：

MS believes MS received H(MR,PW) （6）

根据式（5），Ax10，Nec可得：

PS believes PS sees H(PW,PR) （7）

根据式（6），Ax10，Nec可得：

MS believes MS sees H(MR,PW) （8）

根据P1，Ax17可得：

PS believes fresh H(PW,PR) （9）

根据P2，Ax17可得：

MS believes fresh H(MR,PW) （10）

根据式（5），P3，P6，P9，Ax4，Ax14，Nec可得：

PS believes MS said H(PW,PR) （11）

根据式（6），P4，P5，P10，Ax4，Ax14，Nec可得：

MS believes PS said H(MR,PW) （12）

根据式（9），（11），Ax19可得：

PS believes MS says H(PW,PR) （13）

根据式（10），（12），Ax19可得：

MS believes PS says H(MR,PW) （14）

综上所述，目标T1可由式（7）、（13）得到；目标T2可由式（8）、（14）得到。

3.2 WBAN_DPAP协议其他安全性

本协议是基于动态口令和非对称密码学的无线体域网认证协议。不断变化的因素将作为动态因子加入到认证过程中形成动态口令，计算量小，与静态口令相比具有随机性、动态性、一次性。非对称加密不需要在通信前同步密钥，与对称加密相比安全性更好。因此，WBAN_DPAP协议是轻量的并且具有高安全性。具体分析如下：

（1）实现双向认证。在协议认证过程中，当MS计算 B=H(MR′//PW)与 PS发送的 A=H(MR//PW)相等时，PS是合法的；当PS计算D=H(PW//PR′)与MS发送的C=H(PW//PR)相等时，MS是合法的。若有其中一方结果不相等，则实体为非法用户，由此可实现协议实体的双向认证。

（2）阻止重放攻击。协议认证过程包含的随机数PR、MR，时间戳T1、T2均为一次有效的动态因子，保证了消息的不可重用。即使被拦截，攻击者获取消息并进行重放也将花费一定时间，时延超过ΔT，实体拒绝接受认证请求。因此可以抵抗重放攻击。

（3）阻止伪装攻击。攻击者伪装合法实体进行攻击，包括伪装PS实体和伪装MS实体两种情况。如果攻击者试图伪装PS实体登录医疗服务端获取服务，则必须计算对应的A=H(MR//PW)。由于攻击者未在服务器端注册，无法获得第一次认证所需的MR，因此不能伪装成PS实体。若攻击者尝试伪装MS实体获取用户敏感资源或数据，必须计算对应的C=H(PW//PR)，由于攻击者不可能得到MS的私钥，无法解密PS实体发送的消息也就无法获得随机数PR，故无法伪装为MS实体。因此协议能够有效阻止伪装攻击。

（4）阻止拒绝服务器攻击。假设协议过程中没有加入时间戳，PS实体和MS实体收到消息未加判断即进行私钥解密操作，容易导致耗尽资源而拒绝服务。WBAN_DPAP协议中加入时间戳，实体收到消息后首先进行判断，若时延超过ΔT，则拒绝认证，因此协议能有效抵御拒绝服务器攻击。

（5）阻止口令离线攻击。在整个协议交互过程中，PS和MS实体之间的认证消息是由随机数、时间戳等因子经过复杂的数学运算和加密运算得到的，消息间不存在运算关系，且消息中运用的散列函数是单向的安全散列函数。若试图使用穷举法，巨大的计算量将会使攻击者束手无策。

4 基于SPIN的WBAN_DPAP协议分析

4.1 SPIN模型检测工具

Promela语言解析器SPIN（Simple Promela Interpreter）是由美国贝尔实验室Gerard J.Holzmann开发的用于验证通信协议的模型检测工具。工具采用深度优先搜索遍历状态空间，以Promela作为建模语言，使用线性时态逻辑（Linear Temporal Logic，LTL）公式描述系统需求。SPIN模型检测工具可以提供系统语言用于直观准确地描述系统模型而不考虑具体实现细节，功能强大而简明地描述系统应满足的属性，提供了一套验证系统建模逻辑一致性及系统是否满足所要验证性质的方法。SPIN的协议验证模型如图3所示。

图3 SPIN协议验证模型

如图3所示，SPIN的协议验证模型包括三个阶段：设计阶段、建模阶段以及验证阶段。在协议设计阶段，根据无线体域网环境的特点设计一种适用于无线体域网的认证协议；协议建模阶段包括两方面，一方面使用Promela语言编写描述系统行为的模型，另一方面采用LTL公式表达系统要求的安全性属性；在协议验证阶段，使用SPIN对协议进行分析，经语法分析没有错误后对系统交互进行模拟，直到确认协议设计拥有预期的行为。如果SPIN在验证过程中发现模型不满足LTL公式描述的目标属性，则表明所验证的协议存在缺陷或攻击，这时跟踪trail文件可以得出反例，可由人工进行诊断，返回设计阶段找出错误原因[16]。

4.2 WBAN_DPAP协议的SPIN检测分析

本次协议的SPIN检测分析实验环境为：Windows10操作系统、SPIN版本为6.4.9、iSpin版本为1.1.4，TclTk版本为8.5。

用Promela对WBAN_DPAP协议的实体进行建模以模拟协议运行过程。PS、MS和入侵者Intruder三者身份分别用AgentP、AgentM、AgentI表示；通信对象partner包括 PS、MS 和Intruder；Msg1和Msg2为协议认证过程中两个不同的消息，分别表示WBAN_DPAP协议中实体PS和MS发送的消息；statusP、statusM表示协议认证执行结束后MS和PS的状态，为布尔类型值。MS、PS的建模如图4所示[17]。

图4 PS与MS的通信建模示意图

如图4所示，主体PS选择通信对象partner并向通道中发送消息Msg1，该消息由主体MS接收并选择通信对象partner后回应消息Msg2。双方在协议顺利完成，即没有攻击者参与的情况下将各自状态statusP、statusM设置为OK。

对WBAN_DPAP协议进行Promela描述后，为了验证建模的正确性及协议运行的过程，使用SPIN模型检测工具模拟协议各主体的通信行为，如图5协议行为模拟图所示，在没有入侵者存在的情况下，可以成功地模拟协议执行顺序，达到协议所期望的目的。

图5 无入侵者时议通信行为模拟图

从图5中可以看出，该协议共创建两个进程，从左至右分别为PS、MS两个进程，分别表示个人服务器和医疗服务端进程。系统为每个进程赋予一个唯一的进程号Pid，PS实体进程号为0，MS实体进程号为1。PS首先向MS发送消息Msg1，MS收到消息后返回消息Msg2，由此可知协议执行顺序与协议设计一致。

在WBAN_DPAP协议中，PS与MS实体间完成相互认证，需要满足协议安全性的LTL公式表示如下：

其中，&&表示与运算，[]P表示P在所有状态点都成立，<>P表示P最终会在某些状态点成立。

采用Dolev-Yao模型对非法攻击者Intruder进行建模。攻击者在协议通信过程中窃取消息并进行存储，然后选择一个消息接收者进行消息的重放。攻击者的Promela建模示意图如图6所示。

图6 Intruder的通信建模示意图

从图中可以看出，攻击者通过截获PS与MS之间通信的消息达到攻击目的。加入攻击者模型后，对协议需满足的LTL属性进行验证，验证结果如图7所示。图中“Full statespace search for”表示默认为完全的状态空间搜索。“State-vector 64 byte，depth reached 26”表示完全描述一个全局系统的状态需要64 Byte的内存，最长深度优先搜索路径包含26个从树根开始的转移。“errors：0”表示在这次搜索过程中没有发生错误，即协议满足LTL公式描述的属性。“128.730 total actual memory usage”表示该协议进行检测时数据使用的内存空间总字符为128.73 MB[18]。

图7 协议验证结果图

5 结束语

本文在前人基于生物信息和传统密码学的研究基础上，提出一种适用于无线体域网的动态口令双向认证轻量级协议。通过理论证明和SVO逻辑推理方法验证了WBAN_DPAP认证协议的安全属性。使用SPIN模型检测工具对协议进行建模实验，实验结果表明，WBAN_DPAP认证协议满足安全性目标。

该协议将时间同步认证机制与一次性密码相结合，使用时间戳和随机数作为双重身份验证因素，采用非对称加密算法对通信消息进行加密，整个方案安全性更高且轻量。下一步工作，继续研究本文提出的无线体域网认证协议的资源占用率和能耗，在保证安全的前提下，进一步减少其资源消耗。