协议组合逻辑安全的4G无线网络接入认证方案

王丽丽，冯涛,2,，马建峰

(1. 兰州理工大学 计算机与通信学院, 甘肃 兰州 730050;2. 福建师范大学 网络安全与密码技术重点实验室, 福建 福州 350007;3. 西安电子科技大学 计算机网络与信息安全教育部重点实验室, 陕西 西安 710071)

1 引言

在多种无线通信技术及异构网络共存、融合的趋势下，4G无线网络移动终端的安全接入问题变得更加复杂和重要[1]。2009年，ITU-R确立了两大4G候选标准：LTE-Advanced和IEEE 802.16m。文献[2,3] 中介绍了关于 LTE RAN(radio access network)的安全决策，但没有给出具体的接入认证协议。文献[4]中，IEEE 802.16m工作组针对4G网络的安全机制提出了PKMv3(privacy key management version 3)协议，但也没有给出具体的接入认证过程。

1991年，Girault首次提出自证实公钥系统[5]。同基于证书的公钥密码体制相比，自证实公钥系统更适用于移动环境。首先，AN(access network)和ME(mobile equipment)的认证参数中不包含公钥证书，协议交互之前，不需要存储和传送自己的公钥证书，不需要验证彼此公钥证书的合法性和有效性，节省了存储空间和通信带宽，减轻了网络负载和传输时延，减少了移动终端的计算负担；此外，对公钥的验证隐藏在签名验证或加密过程中，当网络存在阶层关系时也不需要通过其他网络实体转发认证信息，提高了公钥验证效率和认证效率。

Zheng等人[6]基于自证实公钥系统提出了一个4G网络用户认证方案，但方案还存在不足之处。第一，方案中，网络端的公钥并不是基于自证实公钥系统构建的，对该公钥的验证是利用基站联合广播，并在ME中设立缓冲区，通过概率统计方法实现的。但是验证结果存在风险，如局部出现伪基站密度超过合法基站的可能等。而且，方案中没有明确指出如何确定终端缓冲区的长度、如何确定伪基站与合法基站的数量同识别成功的概率之间的关系。第二，该方案的首次接入认证和切换认证协议中，用户的归属环境和访问网络之间需要交互部分认证信息，接入时延会增加，对实时应用很不利。第三，Zheng没有对该方案的安全属性进行形式化分析和证明。

考虑到4G网络中ME的安全接入问题，以及ME的移动性和漫游性，本文基于自证实公钥设计了一个新的4G无线网络终端接入方案，方案包括首次/切换接入认证协议和再次接入认证协议。由于安全协议的分析和证明对于现代安全网络系统至关重要，通过运用DDMP理论[7]，本文给出新方案的演绎推导，并对其安全属性进行了形式化证明和分析。DDMP理论由A.Datta等人[7]提出，它包括协议演绎系统PDS和协议组合逻辑PCL，该理论既可以作为协议设计的新方法，又为协议的安全性证明和分析提供了一种全新的形式化方法。

2 预备知识

2.1 自证实公钥系统

TA(trust authority)公开模数n及其公钥e，秘密保留私钥d，用户的注册过程如下[5,8]。

1) 用户选定长度为160bit以上的私钥x，并计算出V=g-xmodn，n是长度为1 024bit以上的模数，然后将V和自己身份ID传给TA。

2) TA计算用户的公钥Y，Y=(V-ID)dmodn，并将Y传给用户。

3) 用户验证V=(Ye+ID)modn，若等式成立，则用户的公钥为Y，私钥为x。

在自证实公钥系统中，用户的身份、公钥和私钥满足一种计算上不可伪造的数学关系，在利用密钥执行加解密、签名验证、密钥协商或其他密码操作的同时，就可以验证该数学关系，从而验证公钥的合法性和有效性。用户的私钥是自己选定的，其安全性基于解离散对数困难问题，TA无法从传送过来的数据中得到用户的私钥，不能冒充用户伪造他们的签名，相比于基于身份的公钥密码体制，具有更高的安全性，更适合于开放系统环境中的应用。此外，TA无法完全掌握公钥的产生和验证，即使TA伪造出相同用户的另一个公钥也会被检测出来。

2.2 协议演绎系统和协议组合逻辑

协议演绎系统(PDS)由构件集合和操作集合组成，构件是用于构造复杂协议的简单协议，操作集合包含3类不同的演绎操作：组合、求精和转换。组合操作用于2个协议的组合，包括并行组合和串行组合。求精操作用于一个简单协议构件上，为协议添加必要的安全属性，且不会改变协议的消息数或协议的基础结构，例如用加密的随机数代替原来没有加密的随机数。转换操作则是通过移动消息、组合协议步骤、插入一个或多个协议步骤等操作完成对协议的修改，例如将数据从一个消息移动到另外一个较早的消息中。本文中主要使用的演绎操作包括串行组合操作、转换操作T1以及求精操作R3、R4和R6(具体含义在本文设计的安全协议演绎过程中说明)。

协议组合逻辑(PCL)可用于安全协议的形式化证明和分析，同BAN逻辑及其他的逻辑方法相比，PCL支持安全协议的组合证明；由于包含了协议的执行过程，PCL不需要对协议进行抽象；PCL采用的是标准逻辑概念，而不需要使用“管辖(jurisdiction)”和“信念(belief)”等不清晰规则。此外，PCL加入了密码学原语，并重点刻画了消息的发送和接收，这些概念体现了安全协议的基本要素。目前，PCL已经被成功用于形式化证明多个协议的正确性，如SSL/TLS协议[7]、IEEE 802.11i协议[9]、Kerberos V5 协议[10]等。

PCL的基本语法元素是前置断言—后置断言表达式，即几乎所有的安全协议证明步骤都遵循θ[P]Xφ规则，该规则表明协议的执行实例X执行动作序列P以后，状态由θ转变为φ。本文用到的部分公理和法则如下[7,11,12]。

Contains(t1,t2)：表示t1包含t2。

Fresh(X,t)：表示在实例X中产生的t是新鲜的。

Has(X,t)：秘密属性的一种描述，表示实体Xˆ在实例X中拥有信息t。

Honest(Xˆ)：表示实体Xˆ在当前轮中是诚实的，其执行的所有动作都是协议所规定的。

Send(X,t)/New(X,t)/Sign(X,t)/Encrypt(X,t)：分别表示发生了发送、生成随机数、签名和加密动作。

3 4G无线网络接入认证新方案

3.1 参数描述

相关参数要求[5,8]：|x|表示x的长度，整数A、B、S满足其中，|S|表示私钥长度。TA为ME产生自证实公钥的过程如下。

1) ME选定私钥MEx，计算并将IDME、IDHE和VME发送给TA，其中，IDME是ME的身份标识符(IMSI)，IDHE是ME的归属环境HE(home environment)的标识符。

同理，AN通过TA获得公钥YAN，私钥ANx。

3.2 移动终端的首次/切换接入认证协议

为了满足移动网络的需求和特性，针对用户在首次接入、再次接入和漫游切换等不同场景，本文基于自证实公钥系统提出了首次/切换接入场景下的认证与密钥交换协议(AKEBSP,authentication and key exchange protocol based on self-certified public key)和再次接入场景下的认证协议，在确保安全接入的前提下，提高了认证效率。首次/切换接入场景下的认证过程如图1所示。

图1 首次/切换接入认证过程

此过程说明如下。

1) ME收到AN广播的IDAN和公钥YAN后，选择随机数并将cME、IDAN、IDHE发送给AN。

2) AN验证IDAN后，选择随机数rAN∈[ 0,A]和cAN∈[ 0 ,B]，分别计算TAN=rAN+xANcME和RAN=grANmodn，并将消息cAN、RAN、RAN、SigAN发送给ME，其中SigAN= {cME,cAN,RAN,TAN}xAN。

3) ME首先验证SigAN，如果正确，则验证下面式子是否成立：和TAN∈[0,A+(B-1)(S-1)]。如果成立，则选择随机数rME∈ [ 0,B]，并计算然后将消息发送给AN。

5) ME收到消息并解密，获得了自己的临时身份TIDME，供再次接入该网络使用。

认证结束后，AN会在数据库中存储TIDME和（IDME,YME,KAM）的对应关系，向ME提供服务后可以将作为不可否认凭证发送给ME的归属环境HE。其中，bill为计费信息，

3.3 移动终端再次接入认证协议

首次/切换接入认证通过后，ME需要再次接入到同一网络时，可以利用TIDME代替协议中的IDME进行再次接入认证，保护了ME的身份隐私，其认证交互过程如图2所示。其中，TIDME′是AN为ME生成的新的临时身份，KAM′是AN生成的新的会话密钥，作为ME和AN下次交互使用，减少了攻击者通过已攻陷的会话密钥同网络交互的风险。

图2 再次接入认证过程

4 新协议的演绎

由于篇幅限制，本文仅对首次/切换接入场景下的认证与密钥交换协议 AKEBSP进行演绎推导和形式化证明。在新协议的演绎过程和步骤中，为了简洁和清晰，分别用Xˆ和Ŷ表示协议的2个参与方：移动终端ME和接入网络AN，其相应的实体分别用X和Y表示。此外，AN的公钥也可用Ŷ表示，终端的归属环境标识符用IDH表示。

首先，选取3个简单的基本协议，一个是基于签名的挑战应答协议P1，另外2个是基于加密的挑战应答协议P2 和P3（其中，Ŷ是AN的公钥，密钥K是ME通过RY计算得到的）。

对协议P1 和P2进行串行组合（串行组合操作是通过适当的替代步骤，使前一协议模块的输出代替后一协议模块的输入来完成协议的组合），用协议P1 的输出代替P2的输入，从而得到协议P4。

对协议P4应用转换操作T1（通过将数据从一个消息移动到另外一个较早的消息中），将cY移动到较早的消息中，从而得到协议P5，其主要目的是减少消息数量。

由于ME验证AN时需要使用2个参数，分别是由RAN=grANmodn和TAN=rAN+xANcME计算得到的RAN和TAN，但协议P5中并未给出，根据转换操作的定义，这里可以应用转换操作在协议第二步中加入RAN和TAN，从而得到协议P6。

为了让X确信消息是由Y新鲜生成的，对协议P6应用转换操作T2，得到协议P7，其主要目的是为了防止重放攻击。

由于ME要明确接收消息的AN，并需要同归属环境进行交互，根据转换操作的定义，在协议第一步中加入IDY和TIDH，从而得到协议P8。

对协议P8 和P3进行串行组合，用协议P8 输出代替协议P3的输入，从而得到协议P9。

对协议P9应用转换操作T1，将消息RX移动到较早的消息中，从而得到协议P10，其主要目的也是减少消息数量。

由于AN验证ME时还需要参数TX、X的身份标识IDX以及X的公钥YX，但协议P10中并未给出，根据转换操作的定义，这里可以应用转换操作在协议第3步中加入TX、IDX和YX，从而得到协议P11。

为了保护用户的身份隐私，首次认证或切换认证之后，用户再次接入该网络时是借助一个临时身份TIDX，但协议P11中并未给出，根据转换操作的定义，这里可以应用转换操作在协议第4步中加入TIDX，从而得到协议P12。

到此为止，通过协议演绎系统(PDS)演绎得到了新协议AKEBSP。

5 新协议安全性的形式化证明和分析

5.1 协议流程表示

PCL标记法表示的协议角色如下。

其中，InitAKEBSP是发起者角色(对应于 ME)的动作序列，RespAKEBSP是响应者角色(对应于AN)的动作序列。

5.2 安全属性的形式化证明

定理 1 AKEBSP安全认证协议具有会话认证性。

根据协议组合逻辑PCL，需要证明的发起者角色会话认证性的形式化表示为

当上式成立时，AKEBSP协议的发起者角色能够保证会话认证性。这里仅给出ME端的证明情况，AN端的证明情况类似。

证明

定理2 AKEBSP安全认证协议具有密钥机密性。

根据协议组合逻辑PCL，需要证明的发起者角色密钥机密性的形式化表示为

当上式成立时，AKEBSP协议的发起者角色能够保证密钥机密性。这里仅给出ME端的证明情况，AN端的证明情况类似。

证明

5.3 新方案的综合分析

从认证协议的可证明安全性、通信效率和计算效率等方面对新方案中的 AKEBSP协议和文献[6]提出的SPAKA协议进行比较，结果如表1所示，其中有关符号说明如下：|SV|表示一次签名验证操作，|SED|表示一次对称密钥加解密操作，|PED|表示一次非对称密钥加解密操作。

新方案是基于自证实公钥系统提出的，节省了存储空间，减少了ME的计算量和认证时延。根据协议的演绎过程可知，ME和AN之间传递的所有消息均具有新鲜性和不可预测性，所以新方案能抵御重放攻击。

表1 本方案与相关方案的比较

新方案能提供不可否认服务，整个系统中只有拥有正确私钥的终端用户才可以根据cAN构造出合法的TME，一旦终端用户通过了认证，则不能否认自己的接入。当出现纠纷的时候，AN可以提供RAN、TME和cAN进行验证，以作为不可否认凭证。

新方案中，ME的身份（IDME/IMSI）是在用户验证接入网络的身份之后发送出去的，没有以明文形式在空中接口和有线链路传输，且只有TA知道用户公钥和用户身份的对应关系，攻击者无法对用户进行非法跟踪，提供了身份保护。每次认证后，AN都会动态更换用户的临时身份，使得用户身份的安全性大大增强。

6 结束语

本文分析了4G无线网络中移动终端的安全接入认证问题，基于自证实公钥设计了一个新的终端接入认证方案。新方案包括首次/切换接入场景下的认证及密钥交换 AKEBSP协议和再次接入场景下的认证协议，适应了4G无线网络的移动和漫游特性。本文应用DDMP理论中的协议演绎系统PDS对新协议进行了演绎推导，用协议组合逻辑 PCL对协议进行了形式化证明，并综合分析了协议的安全性能。结果表明，新方案具有会话认证性和密钥机密性，不仅能抵御伪基站攻击和重放攻击，还能提供不可否认服务和身份隐私性，同时提高了移动终端的接入效率。

[1] PIYUSH G,PRIYADARSHAN P.4G-A new era in wireless telecommunication[EB/OL]. http://www.idt.mdh.se/kurser/ct3340/ht09/ADMI NISTRATION/IRCSE09-submissions/ircse09_submission_13.pdf, 2009.

[2] AQSACOM S,AQSACOM I. Lawful interception for 3G and 4G networks[EB/OL].http://www.aqsacomna.com/us/articles/Aqsacom_White_paper_4G_LI_v1.pdf,2010.

[3] 3GPP. Technical Specification Group Services and System Aspects;Rationale and Track of Security Decisions in Long Term Evolved(LTE) RAN/3GPP System Architecture Evolution(SAE)(Release 9)[S]. Tech Spec 3GPP TS 33.102 V9.0.0. 2009.

[4] IEEE P802.16m. Part 16:air interface for fixed and mobile broadband wireless access systems[EB/OL].http://lichun.cm.nctu.edu.tw/pa pers/P80216m_D4.pdf,2010.

[5] GIRAULT M. Self-certified public keys[A]. Eurocrypt’91 [C]. Brighton UK,1991.490-497.

[6] HE D K, WANG J,ZHENG Y. User authentication scheme based on self-certified public key for next generation wireless network[A].IEEE International Symposium on Biometrics and Security Technologies [C]. Islamabad, Pakistan, 2008.

[7] DATTA A. Security Analysis of Network Protocol: Compositional Reasoning and Complexity Theoretic Foundations[D]. Computer Science Department, Stanford University, 2005.8-72.

[8] POUPARD C,STERN J. Security analysis of a practical on the fly authentication and signature generation[A]. Eurocrypt’1998[C]. Espoo Finland, 1998. 422-436.

[9] HE C,SUNDARARAJAN M,DATTA A. A modular correctness proof of IEEE 802.11i and TLS[A]. CCS2005-12th ACM Conference on Computer and Communications Security[C].Alexandria,VA, United States,2005.2-15.

[10] ROY A,DATTA A, DEREK A. Secrecy analysis in protocol composition logic[A]. The 11th Asian Computing Science Conference [C].Tokyo,Japan,2006.197-213.

[11] DATTA A, ROY A, MITCHELL J. Protocol composition logic(PCL)[J]. Electronic Notes in Theoretical Computer Science, 2007,172(1): 311-358.

[12] CAS C. On the protocol composition logic PCL[A]. Preceedings of 2008 ACM Symposium on Information, Computer and Communications Security[C].Tokyo, Japan, 2008.18-20.