顾兆军,刘东楠
1(中国民航大学 信息安全测评中心,天津 300300)2(中国民航大学 计算机科学与技术学院,天津 300300)
飞机降落后停靠停机位时,向航空公司提交飞机健康管理数据、电子飞行包等关键数据,目前大部分机型及航空公司采用人工拷贝及GateLink的方式进行数据传输.随着航电技术和无线技术的发展,Boeing等公司在新机型(如Boeing 787)中装载了无线终端网络模块(TWLU,Terminal Wireless LAN Unit),即机载天线,飞机与航空公司的数字通信可以使用机载天线和布置在廊桥上的无线接入点,该过程采用802.11协议.传统无线网络采用有线等效加密(Wired Equivalent Privacy,WEP)及Wi-Fi保护访问(Wi-Fi Protected Access,WPA)的加密方式,目前WEP、WPA、WPA2均被攻破.故在飞机与廊桥AP进行数据传输时,需要一种更安全的身份认证方式.
1985年,Victor Miller和Neal Koblitz首次提出将椭圆曲线密码体制(Elliptic Curves Cryptography, ECC)的离散对数问题应用到加密中[1,2].因ECC不存在亚指数时间算法,在相同安全强度下具有更小的密钥尺寸、更快的运行速度、抗攻击性强等特点,近年来被越来越多地应用到数字签名、身份认证及无线网络和机载网络中.俞惠芳等将身份混合签密与双线性映射结合提出了ECC身份混合签密方案[3];周志彬等将ECC应用到了RFID身份认证中[4],以Nam J为代表的研究团队将ECC应用到了无线网络中,从而增强无线网络数据传输的安全性[5],黄后彪将ECC与机载无线移动自组织网相结合[6],以解决机载网络身份认证和密钥协商的问题;李建华等对当前主流网络安全协议的形式化验证做出了详细的分析[7].此外,还出现了基于零知识证明的身份认证方案,如文献[8].
本文结合民航信息系统的特点及飞机健康管理数据、电子飞行包等数据在传输过程中所需的安全需求,利用椭圆曲线密码技术,提出一种数字签名技术,并首次提出一种用于飞机与航空公司间的身份认证方案,将该认证接入到某民航专用模拟系统中,使用SVO逻辑对该方案进行形式化验证,确保该方案的可行性及有效性.
2.1.1 ECC相关知识
定义1. 有限域.设p是一个素数,Fp由{0,1,2,…,p-1}中p个元素构成,称Fp为有限域.
定义2. 有限域上的椭圆曲线.有限域Fp上的椭圆曲线是由点组成的集合.在仿射坐标系下,椭圆曲线上点P(P≠O)的坐标为P=(xp,yp),其中xp,yp为满足一定方程的域元素,为点P的x坐标和y坐标.
定义3. 阶.Fp(p是素数,p>3)上一条椭圆曲线的阶是指点集E(Fp)中元素的个数,记为#E(Fp).由Hasse定理知,p满足下述条件:
(1)
在素域上,若一条曲线的阶#E(Fp)=p+1,则称此曲线是超奇异的,否则称为非超奇异的.
定义4. ECC的离散对数问题(ECDLP).已知椭圆曲线E(Fq)、阶为n的点P∈E(Fq)及Q∈
,椭圆曲线离散对数问题是指确定整数l∈[0,n-1],使得Q=[l]P成立.
定理1. ECC的加法乘法运算.
域元素的加法是整数的模p加法,即若a,b∈Fp,则a+b= (a+b) modp.
域元素的乘法是整数的模p乘法,即若a,b∈Fp,则a·b= (a·b) modp.
ECC的加法乘法运算变换如图1所示.
图1 ECC中加法和乘法运算Fig.1 Addition and multiplication of ECC
定理2. ECC的多倍点运算.设k为一个正整数,P是椭圆曲线上的点.称点P的k次加为P的k倍点运算,记为:Q=[k]P=P+P+…+P.
2.1.2 ECC加密流程
1)ECC中各数据类型转换关系如图2所示.
图2 数据类型和转换约定Fig.2 Data types and transformation agreed rules
2)基于ECC的一般数据加密过程
Step1.节点A在选定的椭圆曲线EP(a,b)上找一点G作为基点.
Step2.节点A选择私钥k,生成公钥K=kG.
Step3.节点A将三元组
Step4.节点B收到消息后,将明文编码到EP(a,b)上一点M上,生成随机数r(r Step5.节点B计算:C1=M+rK,C2=rG,并传给节点A. Step6.用户A接收到消息后,计算C1-kC2,结果为M. 本方案采用一种组合式伪随机数发生器生成认证过程中所需的随机数,该方法能有效解决随机数中常见的“重复值”的问题,大大降低了出现相同随机数的概率,能够有效抵抗重 图3 伪随机序列生成Fig.3 Generation of pseudo random sequences 放攻击.SEED进入随机数发生器后,首先由杂凑函数Hv()计算后生成伪随机序列,从该序列中任选两个值,作为EP(a,b)的基点及倍数,进行多倍点运算,最后计算出K值,即为新的随机数.伪随机序列生成过程如图3所示. 3.1.1 Gatelink数据传输的缺点 GateLink传输方式分为红外连接及有线连接两种方式,存在易受外部环境影响、硬件成本高等问题;人工拷贝的方式存在工作效率低、安全性差等问题.GateLink数据传输及廊桥AP数据传输方案如图4所示. 图4 三种数据传输方式示意图Fig.4 Diagram of 3 kinds of data transmission mode 3.1.2 面向廊桥AP数据传输的安全需求 面向廊桥AP的数据传输只允许来自机载天线的连接.在应用层面,廊桥AP连接传输数据类型及功能单一,只用于传输电子飞行包等关键数据,且安全需求极高;该连接可以在需要时开启,即飞机舱门开启后开始进行数据传输.而传统无线网络,一般情况下不能随时开启,所有终端均可接入,传输数据种类多,应用广泛,安全需求不高.故在本方案中,飞机接入网络后,首先识别文件签名及文件类型,拒绝非法节点接入及数据传输.下面对廊桥AP的安全需求进行分析,传统无线网络需满足数据传输的保密性、完整性及可靠性,面向廊桥AP的数据传输还应保证认证实体的双向认证、不可否认性及可审计性等. 1)双向认证 在飞机与廊桥AP数据传输过程的认证方案中,由于传输的数据敏感度高、安全需求大,在身份认证过程中需要精确的辨识度,故机载天线与廊桥天线需要进行双向认证,以防止重放攻击及无关AP的偶然连接或恶意连接. 2)不可否认性 在数据传输过程中,由于传输数据的特殊性,需要一种技术确定数据来源及其不可否认性,即每个实体在通信过程中都要具有唯一身份标识. 3)可审计性[12] 在面向廊桥AP的数据传输中,要求每个实体的行为均可被追踪到.一旦发生安全事故,可根据审计记录追寻入侵过程. 本方案由三个认证实体组成,分别为:飞机(A)、航空公司(HK,即廊桥节点)及认证中心(CA).飞机和廊桥节点首先通过CA进行注册,然后进行双方认证,在认证过程中需要使用用户唯一身份标识. 认证过程中出现的符号如表1所示. 表1 符号说明Table 1 Symbol explanation 1)签名生成 飞机节点A生成数字签名的方法如下: Step1. 飞机的身份为IDA,IDA的长度为ENTLA,a,b为椭圆曲线方程参数,G为在椭圆曲线上选取的基点,待签名消息为M,选取的椭圆曲线方程为: Ep(a,b):y2=x3+ax+b (2) ZA=Hv(ENTLA‖IDA‖a‖b‖xG‖yG‖xA‖yA) (3) (4) Step3. 随机数发生器生成随机数k∈[1,n-1],计算椭圆曲线点(x1,y1)=[k]G Step4. 计算r=(e+x1)modn Step5. 判断:若r=0或r+k=n返回. Step6. 计算 s=((1+dA)-1·(k-r·dA))modn (5) Step7. 判断:若s=0返回Step 3. Step8. 消息M的签名即为(r,s). 2)签名验证 机场节点B收到的来自飞机节点A的消息为M′,数字签名为(r′,s′),验证方法如下: Step1.判断:r′∈[1,n-1]及s′∈[1,n-1]是否同时成立,若不同时成立,则验证不通过. (6) Step3.计算 t=(r′+s′)modn (7) Step4.判断:若t=0,则验证不通过. Step5.计算椭圆曲线点 (8) Step6.计算 (9) 判断:R=r′,若成立则验证通过,否则验证不通过. 3.4.1 注册阶段 当飞机节点通过机载天线与廊桥AP连接向机场进行传输数据时,首先要在CA注册该节点合法,飞机节点由CA生成公钥,并自行生成私钥,最后通过CA向机场方证明其身份,飞机节点向CA注册过程如下: Step1. 飞机节点由随机数生成器生成随机数k1,计算: V=hv(k1,IDA)·G (10) 将IDA和V发送给CA. Step2. CA由随机数生成器生成随机数k2,计算飞机节点A的公钥,将飞机节点地公钥及w传给飞机节点. PA=V+(k2-hv(IDA))·G (11) w=k2+dCA(XPA+hv(IDA))modn (12) Step3. 飞机节点收到公钥后,计算私钥,并验证公钥的有效性. dA=w+hv(k1,IDA)modn (13) dA·G=PA+hv(IDA)·G+(XPA+hv(IDA))PCA (14) Step4. 若上述等式成立,则飞机节点注册成功,公钥和私钥分别为PA、dA. 飞机节点向CA注册后,拥有其公钥和私钥.公钥由CA负责管理,其它节点可以通过CA获得;私钥由飞机节点自行管理,不能透漏给其它节点. 3.4.2 认证阶段 当飞机到达具备廊桥AP的机场时,舱门打开后连接开始建立,飞机节点(A)、廊桥节点(B)在CA注册成功后,开始进行身份认证,过程如图5所示. Step1. 飞机节点向廊桥节点发布自己的身份信息IDA、公钥PA及TA,TA为由随机数k3经过ECC变换后的值,即: TA=k3·G (15) Step2. 廊桥节点接收到飞机节点的身份及其它信息后,将随机数k4返回给飞机节点. 图5 身份认证过程Fig.5 Authentication process Step3. 廊桥节点将IDB、PB及TB传给飞机节点,TA为由随机数k5经过ECC变换后的值,即: TB=k5·G (16) Step4. 飞机节点将生成的随机数k6发给廊桥节点. Step5. 飞机节点、廊桥节点分别计算VB、yA及VA、yB,即 VB=PB+hv(IDB)·G+(XPB+hv(IDB))·PCA (17) yA=k3+dA·k4(modn) (18) VA=PA+hv(IDA)·G+(XPA+hv(IDA))·PCA (19) yB=k5+dB·k6(modn) (20) Step6. 验证阶段,飞机节点及廊桥节点互相发送yA及yB,结合ECC的性质,判断: (21) 是否成立.在本阶段,Ti、yi、ki均为共享参数,Vi可由CA提供的信息进行计算获得,在验证中,须验证三个式子相等,若出现一方与其它两方不相等,说明认证出现错误或中间人攻击,则验证不成功,若三个式子同时成立,则认证成功,数据传输开始. 4.1.1 相关规则 SVO逻辑使用MP(Modus Ponens)及Nec(Necessitation)两条推理规则及20条公理,如下所示. 1)两条基本推理规则 Modus Ponens:Fromφandφ⊃ψinferψ Necessitation:From ┠φinfer ┠Pbelievesφ 2)SVO逻辑的推理公理 A.信任公理(BelievingAxioms) Pbelievesφ∧Pbelieves(φ⊃ψ)⊃Pbelievesψ Pbelievesφ⊃Pbelieves(Pbelievesφ) B.消息来源公理(SourceAssociationAxioms) (PKσ(Q,K)∧Preceived{X}K-1)⊃QsaidX C.密钥协商公理(KeyAgreementAxioms) D.接收公理(ReceivingAxioms) Preceived(X1,…,Xn)⊃PreceivedXi E.看到公理(SeeingAxioms) PreceivedX⊃PseesX Psees(X1,…,Xn)⊃PseesXi (PseesX1∧…∧PseesXn)⊃(PseesF(X1,…,Xn)) F.理解公理(ComprehendingAxioms) Pbelieves(PseesF(X))⊃Pbelieves(PseesX) (PreceivedF(X)∧Pbelieves(PseesX))⊃Pbelieves(PreceivedF(X)) G.叙述公理(SayingAxioms) Psaid(X1,…,Xn)⊃(PsaidXi∧PseesXi) Psays(X1,…,Xn)⊃(Psaid(X1,…,Xn)∧PsaysXi) H.仲裁公理(JurisdictionAxioms) (Pcontrolsφ∧Psaysφ)⊃φ I.新鲜公理(FreshnessAxioms) freshXi⊃fresh(X1,…,Xn) fresh(X1,…,Xn) ⊃fresh(F(X1,…,Xn)) J.随机数验证公理(Nonce-VerificationAxioms) (fresh(X)∧PsaidX)⊃PsaysX K.共享密钥的对称良好性公理(SymmetricgoodnessofsharedkeysAxioms) L.拥有公理 (HavingAxioms) PhasK≡PseesK 4.1.2 形式化分析 使用SVO逻辑对协议的形式化分析分为四个部分,即初始化假设集、预期目标、推理及证明. 1)初始化假设集 P1:Abelievesfresh(k3,k6) P2:Bbelievesfresh(k4,k5) P3:Areceived(IDB,PB,TB,k4,yA) P4:Breceived(IDA,PA,TA,k6,yB) P5:AbelievesBhas(k5) P6:BbelievesAhas(k3) P7:AbelievesBhas(PB,dB) P8:BbelievesAhas(PA,dA) P9:Bsaid(IDB,PB,TB,k4,yA) P10:Asaid(IDA,PA,TA,k6,yB) 2)预期目标 G1:A确认B是否可连通,即通信认证,可被表述为:AbelievesBsaysM. G2:A与B所发送消息的不可否认性,即AbelievesBsaidM. G3: 证明消息的双向认证,即A与B可进行相互认证,可被表述为:AbelievesAsees(PB,k4,yA),BbelievesBsees(PA,k6,yB). G4:A要确认B发送的消息与近期对话有关,并确定消息及密钥的新鲜性,即B近期发送的消息M,且M中含有A刚刚产生的消息,即实体认证,可被表述为:Abelieves(BsaysM∧fresh(k5)). 3)推理和证明 G1:通信认证 (Abelievesfresh(IDA,PA,TA,k3,k6,yB)∧Asaid(IDA,PA,TA,k3,yB))⊃Asays(IDA,PA,TA,k3,yB). by P2,P10,Nonce-verificationAxioms. 同理可推,B says (IDB,PB,TB,k4,yA) by P1,P9,Nonce-verificationAxioms. G2:消息的不可否认性 AbelievesBsaid(IDB,PB,TB,k4,yA) by P11,BelievingAxioms,SourceassociationAxioms. 同理可推,BbelievesAsaid(IDA,PA,TA,k6,yB). by P12,BelievingAxioms,SourceassociationAxioms. G3:双向认证 Areceived(IDB,PB,TB,k4,yA)⊃AreceivedM AreceivedM⊃AseesM by P3,ReceivingAxioms,SeeingAxioms. 同理可推,BseesM,by P4,ReceivingAxioms,SeeingAxioms. G4:消息及密钥的新鲜性 由G1可得,AbelievesBsaysM. 故,Abelieves(BsaysM∧fresh(k4,k5)). by P2,G1 同理可推,Bbelieves(AsaysM∧fresh(k3,k6)). by P1,G1 通过上述分析,本方案在完成实体通信的同时(G1),可以实现消息的不可否认性(G2)、双向认证(G3)以及确保密钥的新鲜性(G4),从而有效地抵御恶意节点的接入及攻击,确保了方案的可行性和有效性. 4.2.1安全性分析 1)抗重放攻击 为有效避免重放攻击,本方案在认证时采用“非重复值”的方式,飞机节点或廊桥节点均由随机数生成器中产生不同的随机数ki.若攻击者向参与认证阶段的节点发送随机值,该节点将对该值进行验证,计算yi,若验证不成功,则认证失败,故本方案能有效防止重放攻击.目前常见的防止重放攻击的手段还有添加序列号及时间戳,添加序列号要求参与认证的节点保存所有状态信息,需要消耗一定的系统资源,而时间戳要求双方时间保持严格一致,这在跨时区飞行中具有一定的困难度,故不适合民航领域. 2)双向认证 3)不可否认性 为提高在面向廊桥AP数据传输的不可抵赖性,在身份认证过程中,不同阶段的消息在传输时使用不同随机数进行加密,任一实体具备唯一身份标识IDi,形式化证明表示,本协议具备消息的不可否认性. 4.2.2 效率分析 本节结合提出的身份认证协议,将其应用到TWLU数据传输过程,使用Cpp和tcl语言在NS2软件对TWLU数据传输原型系统中的身份认证过程进行实验仿真,并与近年来提出的相关方案进行对比,探究提出的方案在TWLU数据传输中的运行效率以及在民航领域的适用程度,TWLU数据传输原型系统所使用的网络结构如图6所示. 图6 网络拓扑结构示意图Fig.6 Diagram of network topology 本节对近年来身份认证领域相关研究进行了比较,在如图6所示的网络结构中,对文献[9-11]进行仿真模拟,从安全需求、算法通信成本及算法效率等方面对协议进行了比较分析.安全需求方面,考虑认证方案在抗重放攻击、双向认证、不可否认性及密码强度的实现情况;算法效率方面,对比了协议双方的通信次数(EC)、杂凑运算次数(EH)以及完整协议的运算次数(EP),实验结果如表2、表3所示. 表2 身份认证协议安全性对比Table 2 Security comparison 实验分析表明,文献[9]不能满足TWLU数据传输过程所需的抗重放攻击及双向认证,且使用随机数数量过少,不能保证其安全强度;文献[10]提出的抗重放攻击过于理想化,且忽视了密码强度问题;文献[11]不能有效抵御重放攻击.由4.2.1节可知,重放攻击是TWLU数据传输过程的重要威胁,选择具有“非重复”特性的随机数生成方案十分必要.综上,文献[9-11]不能满足TWLU数据传输过程中的全部安全需求,故不适用于该领域,而本文所提出的算法能够满足该过程所需的安全需求,具备较强的安全性,在该领域有着较好的应用. 表3 身份认证协议效率对比Table 3 Efficiency comparison 从安全性及效率两个方面可以得到如下结论: 结论1.相比其它方案,提出的认证协议具备更强的安全性能,可以抵御重放攻击、实现双向认证、具备不可否认性; 结论2.运算效率方面,提出的方案减少了协议的交互次数和运算次数,在杂凑函数运算次数与其它方案持平. 实验结果表明,提出的方案在民航专用系统中的模拟,安全性能优于其它方案,同时减少了协议运行过程中的交互次数运算次数. 本文以机载天线和廊桥AP间使用无线网络进行数据传输为背景,以椭圆曲线密码体制为基础,首次提出一种用于该过程的身份认证方案,解决了飞机与廊桥间没有统一的认证方案的问题.提出一种新的随机数生成方案,在认证的不同阶段使用不同的随机数以保证密钥的新鲜性,从而有效抵御重放攻击;同时,本方案还实现了双向认证,能有效防御恶意节点或伪基站的非法接入.使用SVO逻辑分析表明,本方案可以满足该数据传输中的安全需求;实验表明,本方案的通信消耗适中,无极端值,安全性能达标,且更适用于民航领域,即面向廊桥AP数据传输及其身份认证过程.在未来的工作中,进一步优化时间戳算法,将该技术应用到TWLU数据传输数字签名和身份认证中.2.2 伪随机序列
3 身份认证方案
3.1 数据传输的安全需求
3.2 认证实体
3.3 数字签名
3.4 身份认证过程
4 形式化验证及分析
4.1 基于SVO逻辑的形式化证明
4.2 安全性能及效率分析
5 结束语