协议认证性安全属性测试方法

何云华,杨 超,张俊伟,马建峰

(1.西安电子科技大学计算机网络与信息安全教育部重点实验室,陕西西安 710071; 2.北方工业大学计算机学院信息安全系，北京 100029)



协议认证性安全属性测试方法

何云华1,2,杨 超1,张俊伟1,马建峰1

(1.西安电子科技大学计算机网络与信息安全教育部重点实验室,陕西西安 710071; 2.北方工业大学计算机学院信息安全系，北京 100029)

认证性建立通信双方的信任关系,是安全通信的重要保障.传统的协议测试方法只关注协议功能的正确性,无法满足认证性等安全属性测试的要求.因此,提出了一种针对协议认证性的安全属性测试方法,利用带目标集合的有限状态机模型SPG-EFSM来扩展描述协议安全属性,并在攻击场景分类的基础上设计了认证攻击算法.通过攻击算法找到了Woo-lam协议和μTESLA协议的认证性漏洞,该方法具有可行性、覆盖率高等特点.

协议测试；安全属性；认证性测试；形式化模型；攻击分类

1 引言

通信协议作为网络和分布式应用的基础[1],其固有的复杂性和潜在的敌对环境,使得协议的安全性面临巨大的挑战.大量基于逻辑推理的方法被用来分析、验证通信协议的安全性[2,3],如认证性、保密性、不可否认性和完整性等安全属性.但是,这些方法大多集中在协议规范分析与验证方面,忽略了另一个不可信、不安全因素——协议实现引入的漏洞[4].

最常见的协议实现安全漏洞测试方法是随机测试[5](Random testing),通过注入大量随机、异常或错误的输入到待测协议中来观察系统是否会出现异常,但其测试数据的生成缺乏准确、高效的指导,测试数据的分布不受控制[6].针对该问题,描述协议数据流的测试方法逐步受到了关注,使用上下文无关文法(BNF)[7]或结构化的Frame语法[8]描述消息字段之间的相关性.但是,此类方法不支持有状态转移的协议控制流的建模.数据流与控制流相结合的测试方法成为了进一步的研究热点.Jing C等人[9]对TTCN-3控制流描述模型进行了语法和语义扩展,但所描述的语法变异类型有限.Yamaguchi等人[10]将抽象语法树(AST)和控制流图(CFG)相结合,在实际测试中也获得了较好的效果.但为了满足特定的安全需求,例如认证性或机密性,通信协议往往对协议消息本身进行了加密等处理,存在大量不可知参数,这使得上述测试方法,很难识别消息的各个字段,构造出合适的测试例.因此,设计专用的协议安全属性测试方法是迫切需求的.

但是,此类研究才刚刚起步.Mashtizadeh等人[11]提出密码-控制流模型,该模型假定攻击者能产生消息认证码用于控制流测试.该方法侧重于控制协议状态的跳转和返回,未考虑协议消息构造方法.Shu G等人[12]提出了以协议消息作为其输入/输出参数的协议描述模型,该模型利用密钥K、随机数N等参数组成的元组来表示消息,并建立了用于表示攻击者行为及协议安全属性的攻击者模型.该方法对加密消息具有一定处理能力,但其攻击者模型不能准确的表示协议某些特定的安全属性.例如协议认证性,必须要结合参与者初始认证目标与协议执行完后状态才能准确的描述.另外,该方法没有考虑某些特殊情形,包括一次会话有多个参与者、一个参与者参与多个会话、拥有合法身份的攻击者参与会话等情形.

针对以上问题,本文提出了协议认证性安全属性测试方法.首先提出一种描述协议安全属性的有限状态机扩展模型SPG-EFSM(Symbolic Parameterized Goal-Extended Finite State Machine),扩展定义参与方目标集,用条件判断函数来对比目标集合与协议执行后的结果,以实现安全属性的验证；在此基础上,对协议攻击场景进行了分类,该分类综合考虑了拥有合法身份的攻击者参与,存在认证中心的多方参与,参与者参与多个会话等情况；然后,结合了Dolev-Yao攻击模型[13],设计了协议认证性攻击算法,该算法包涵了上述所有的分类；最后,通过对广泛应用的Woo-lam协议[14]和μTESLA协议[15]进行了测试,发现存在于Woo-lam协议及其各种更新版本中的已知和未知安全漏洞,以及μTESLA协议的认证漂移问题.

2 SPG-EFSM模型

SPG-EFSM是一种包含安全属性定义和验证的协议描述模型,是Shu G提出的EFSM扩展模型[12]的改进.SPG-EFSM扩展描述了协议目标集合,基于目标集合定义安全属性,通过对比目标集合与协议执行后的结果来指示协议的安全属性是否存在漏洞,该验证规则由条件判断函数来实现.认证性是协议安全属性的重要部分,本文着重对认证性安全属性测试.

定义1、定义2给出了认证目标集、单向认证和双向认证的概念；SPG-EFSM模型的描述由定义3给出.

定义1 认证集一表示为C1={→m|m∈P},→m代表期望认证参与者m身份标识,P为参与者集合；认证集二表示为C2={m→n|m∈P∩n∈P},m→n代表参与者n期望向参与者m认证自己身份标识；参与者n目标集合表示为:

gn={c|((∃c=→m)∈C1∩m≠n)∪

((∃c=m→n′)∈C2∩n=n′);m,n,n′∈P}

(1)

认证结果集定义为R={Succeed,Failed}.

定义2 已知m,n,m′,n′∈P,→n′∈gm,m′→n∈gn.

(1)如果有(m=m′)∩(n=n′),并且协议能正确执行完成,则称协议达到了m认证了n,记m⟹n.

(2)如果有(m⟹n)∩(n⟹m),则称m与n达到了双向认证,记m⟺n.

定义3 SPG-EFSM由七元组组成〈S,A,G,I,O,X,T〉.

其中S——状态集合；

A——原子集合{Key,Nonce,Int}和相应派生规则{E(),H(),MAC(),·},用于描述消息,如E(kT,kab·H(na))；

G——目标集合G={gn|n∈P}；

I——输入集合I=I′∪G,其中I′是原有状态机输入集合；

O——输出集合O=O′∪R,其中O′是原有状态机输出集合；

X——L(A)参数构成的有限集合,具有默认初值,其中L(A)代表由A构成的消息集合；

T——转移过程集合,t=〈s,s′,i,o,p(x,π(i)),a(x,π(i),π(o))〉∈T,其中s,s′分别代表初态、终态,π(i),π(o)分别代表输入、输出的参数,p(x,π(i))是增加了定义2给出认证关系的条件判断函数,a(x,π(i),π(o))是关于变量、输入参数和输出参数的处理过程.

其中,协议的目标集合用于协议的安全属性需求,这里重点考虑认证性.协议认证是通过一个转移过程t=〈s,s′,i,o,p(x,π(i)),a(x,π(i),π(o))〉来验证的,s,s′分别是未认证态、认证态,输入i为G,输出o为R,条件判断函数p(x,π(i))是定义2给出了的认证关系.当p(x,π(i))=0时,未通过认证,o=Failed.a(x,π(i),π(o))表示对消息的处理过程,如对加密消息进行解密、取消息中的某个元素.

为了确保测试有效地实施,协议测试要求状态机模型是确定的可达图[12].定理1证明了SPG-EFSM模型是一个确定的可达图.

定理1 SPG-EFSM是确定性的FSM,并且是一个可达图.

证明 SPG-EFSM可表示为FSM(SG,IG,OR,fnext,foutput)的形式.

其中状态集合:

SG={|(s∈S)∩(V⊆X)∩(gm∈G)}

(2)

输入/输出集合:

IG=G∪L(A),OR=R∪L(A)

(3)

状态转移函数:

fnext:SG×IG→SG,fnext( ,i) =

ttakesmachinefrom

(4)

输出函数:

foutput:SG×IG→OR,foutput(,i)

={o∈OR|∃t∈T,

toutputsORfromuponi}

(5)

3 协议认证攻击算法

3.1 攻击场景分类

为了有效地实施攻击,本节对攻击场景进行了分类.一方面,攻击场景分类可以快速的建立攻击策略,另一方面,攻击分类建立在Dolev-Yao强攻击模型[13]基础上,能够最大化攻击者的能力.本节从是否存在多个参与者、是否利用接收者预言机服务[16]、是否拥有合法身份的攻击者等三个方面对攻击场景进行分类,具体定义如下:

本文用(L-ID,Depend,T)表示攻击情形,其中L-ID为攻击者的合法身份,L-ID=1(L-ID=0)为拥有(无)合法身份；Depend为接收者的预言机服务,Depend=1(Depend=0)为利用(不利用)接收者预言机服务；T为认证中心,T=1(T=0)为存在(不存在)认证中心.

定义4 设A,B为参与者,U为用户集,LU为合法用户集,M为攻击者,Attack为M进行的一次攻击,则Attack可以分为以下八类:

①当(L-CD,Depend,T)=(0,0,0)时,存在Attack1,即:

若M∈U-LU,A,B∈LU,(B→A∈gA)∩ (→A∉gB)∩(→M("A")∈gM),不存在T,协议执行完毕,使得A⟹M("B")或A⟹B.

②当(L-CD,Depend,T)=(0,0,1)时,存在Attack2,即:

若M∈U-LU,A,B∈LU,(B→A∈gA)∩ (→A∉gB)∩(→M("B")∈gM),存在T,如果协议执行完毕,使得A⟹M("B")或A⟹B.

③当(L-CD,Depend,T)=(1,0,0)时,存在Attack3,即:

若M∈U,A,B∈LU,(B→A∈gA)∩ (→A∉gB)∩(→M("B")∈gM),不存在T,如果协议执行完毕,使得A⟹M("B")或A⟹B.

④当(L-CD,Depend,T)=(1,0,1)时,存在Attack4,即:

若M∈U,A,B∈LU,(B→A∈gA)∩ (→A∉gB)∩(→M("B")∈gM),存在T,如果协议执行完毕,使得A⟹M("B")或A⟹B.

⑤当(L-CD,Depend,T)=(0,1,0)时,存在Attack5,即:

若M∈U-LU,A,B∈LU,(B→A∈gA)∩ (→A∈gB)∩(→M("B")∈gM),不存在T,如果协议执行完毕,使得A⟹M("B")或无法完成A⟹B.

⑥当(L-CD,Depend,T)=(0,1,1)时,存在Attack6,即:

若M∈U-LU,A,B∈LU,(B→A∈gA)∩ (→A∈gB)∩(→M("B")∈gM),存在T,如果协议执行完毕,使得A⟹M("B")或无法完成A⟹B.

⑦当(L-CD,Depend,T)=(1,1,0)时,存在Attack7,即:

若M∈LU,A,B∈LU,(B→A∈gA)∩ (→A∈gB)∩(→M("B")∈gM),不存在T,如果协议执行完毕,使得A⟹M("B")或无法完成A⟹B.

⑧当(L-CD,Depend,T)=(1,1,1)时,存在Attack8,即:

若M∈LU,A,B∈LU,(B→A∈gA)∩ (→A∈gB)∩(→M("B")∈gM),存在T,如果协议执行完毕,使得A⟹M("B")或无法完成A⟹B.

3.2 攻击算法

根据定义4,提出了一种通用的攻击算法.该算法是基于主动测试的思想,攻击者Malice可以任意截获和注入消息,攻击者知识集合Ω随攻击过程的进行而增大.针对某一个具体的协议而言,并不是所有Attack都可选择,要根据协议规范{M1,M2,…,MC}来进行选择适合Attack.根据Attack来选取参与者的状态机Mi.例如,双方认证协议规范为{M1,M2},M1,M2分别代表发起者、响应者的状态机,当实施Attack1时,参与者Alice选择M1,Malice选择M2.当涉及到多个session,参与者Alice可能选择多个状态机,用MAi来表示参与者Alice选择第i个状态机.算法通过状态机的推断,转移过程、消息的选择,剔除了不合理的测试分支,提高了算法的效率.

该攻击算法分四个部分:

①选择状态机.先由协议规范{M1,…,MC}确定适当的Attack,再根据Attack来确定用户U的MU、攻击者的MM.

②更新目标集合.目标集合G的更新包括用户gU的更新和攻击者gM的更新,由用户U和Malice选取的状态机在协议中的角色来确定.

③具体攻击.根据当前各状态机的状态进行有针对性的Intercept或Inject.先根据当前各状态机来推断截获或注入的状态机集合MD,再根据MD选择进行Intercept或Inject.如果选择Intercept,就从MD中选取可以进行截取的Mk,然后进行Intercept,并更新Mk和Malice的状态机MD.S,MM.S.如果选择Inject,就从MD中选取可以进行注入的Mk,求得Mk中注入的转移过程Tture,并用lookahead(Ω,Mk.S,X,t)选择可以能产生有效输出的消息,然后更新状态Mk.S,MM.S.

④攻击判断.如果找到认证性的漏洞,算法结束；如果没有找到漏洞,再重复步骤1到步骤4,当尝试超过最大值Max,算法结束.Max是按需设定的尝试次数,用来避免无限测试.

该算法涵盖定义4给出的八种攻击类型.如果该算法可以处理攻击者以合法或非法身份参与,是否利用接收者预言机服务,是否存在认证中心等情况,那么该算法涵盖这八种攻击类型.该算法通过目标集合来表示攻击拥有合法或非法身份的情况.例如,Malice以合法身份与Alice进行通信可表示为:gM={B→M},gB={→M}；Malice以非法身份伪装Alice与Bob进行通信可表示为:gM={B→M("A")},gB={→A}.该算法通过参与者选取多个状态机来表示参与者在不同session中的角色.例如,当Malice截获到Alice发给Bob的消息msg时,发现自己不能阅读,便伪装Alice发msg给Bob以获得预言机服务,这可表示为:gM={A→M("B"),B→M("A")},gA={→B},gB={→A}；当Malice没有利用Bob预言机服务可表示为:gM={A→M("B")},gA={→B}.该算法通过选取{M1,…,MC}中C的取值来表示是否存在认证中心的情况,即多方参与的情况.因此,该算法涵盖了这八种攻击类型.

4 协议的测试与结果分析

4.1 Woo-lam协议描述与测试

Woo-lam协议是经典的认证协议.在此协议中假定Alice和Trent共享对称密钥KAT,Bob和Trent共享对称密钥KBT,协议的最终目标是Alice向Bob证实自己的身份.Woo-lam协议的主要交互过程请参见文献[14].

4.1.1 Woo-lam协议规范描述

SPG-EFSM模型描述Woo-lam协议的协议规范如图1所示.假定攻击者Malice可以截获每一条消息,知道Alice、Bob、Trent从协议开始到结束的每一个状态S,其中S0表示初始状态,SRi表示接受第i条消息,SSi表示发送第i条消息,SA表示认证状态.

4.1.2 Woo-lam协议测试

Woo-lam协议测试结果通过表1给出.攻击者Malice在协议中伪装了Alice与Bob进行会话,Malice以合法身份与Bob进行会话,Malice维护伪装Alice的状态机和合法身份会话的状态机.由于存在两次会话,所以Malice、Bob、Trent分别都存在着两个状态机.从表1可以看出,攻击算法发现了Woo-lam协议存在Attack4,是典型攻击[16]中的平行会话攻击.

表1 检测到Woo-lam协议的认证错误

Woo-lam协议存在Attack4的一个修改方案是在3.Alice→Bob:E(KAT,NB)加入Alice的身份信息,但这种方案也存在攻击,由表2给出.攻击者Malice在协议中伪装了Alice、Trent与Bob进行会话,Malice维护伪装Alice、Trent的状态机,来指导攻击进行.从表2可以看出,攻击算法发现了Woo-lam协议存在Attack2,是典型攻击[16]中的反射攻击.

表2 检测到修改后的Woo-lam协议的认证错误

Woo-lam协议的另一个更新方案是把第4个交互流程改为4.Bob→Trent:E(KBT,Alice·NB·E(KAT,NB)),但这种方案也存在攻击,由表3给出.Bob与拥有合法身份的Malice进行会话时,Malice在协议中伪装了Alice、Trent与Bob进行会话,Malice维护伪装Alice、Trent的状态机以及合法身份会话的状态机.从表3可以看出,攻击算法发现了Woo-lam协议存在Attack4,是典型攻击[16]中的交错攻击.

表3 检测到Woo-lam协议另一更新方案的认证错误

4.2 μTESLA协议描述与测试

μTESLA协议是无线传感器网络中经典的广播认证协议[15],其运行过程包括安全初始化、节点加入、数据包认证等阶段,详细请参见文献[15].

4.2.1 μTESLA协议规范描述

SPG-EFSM模型描述μTESLA协议规范如图2所示.基站(B)的状态机MB位于图2(a)中,先后经历了初始化、接收加入节点请求、给加入节点分发相关参数、数据包发送等过程.节点(N)的状态机MN位于2(b)中,它有五种状态:初始状态、请求加入、接收系统参数、接收基站数据包、认证基站数据包.其中S0、SRi、SSi的定义与4.1.1节相同,pid和sid分别代表了节点和基站的身份标识,Pj表示基站发送的第j个数据包.

4.2.2 μTESLA协议测试

μTESLA协议测试结果通过表4给出.攻击者Malice在协议中干扰基站(Base Station)发给节点(Node)的消息,促使发给节点的消息延时一个时间间隔,也称为“认证漂移”.这个过程可等价于传统有线网络的拦截和转发过程,因此可将此过程表述为:Malice伪装Node接收Base Station的消息,Malice伪装Base Station发送消息给Node.从表4可以看出,攻击算法发现了μTESLA协议存在Attack5.

4.3 结果分析与评估

(1)SPG-EFSM的描述能力分析.

从图1、图2中可以看出,SPG-EFSM模型可以清晰直观地描述Woo-lam协议参与者状态机(MA、MB、MT)和μTESLA协议参与者状态机(MB、MN).协议运行时各参与者之间的认证关系也能被SPG-EFSM模型清晰、准确表现出来.例如在表1中,第二行的gB说明了Bob在本次测试过程中将与Alice建立认证关系,从第三行的gB可以看出Bob又试图与Malice建立认证关系,倒数第二行中给出的A⟹B表明了协议执行完后,达到了Bob认证Alice状态.

表4 μTESLA协议的认证错误

表5 本文攻击算法与其他方法性能比较

(2)攻击算法的性能分析.

令Max=n,协议轮数为m,则该算法的时间复杂度为O(nm),等同于Guoqiang Shu提出算法的时间复杂度.然而,该攻击算法能够表示拥有合法身份的攻击者参与、多个会话和多方参与等特殊情况.与其他方法相比,攻击算法在覆盖率方面也有较大的优势,能够以较少的时间复杂度达到较高覆盖率,如表5所示.

(3)测试方案的新型漏洞探测能力分析.

该测试方案发现了Woo-lam协议及其更新协议当中的漏洞,包括平行会话攻击,反射攻击,交错攻击等典型攻击.测试还发现了μTESLA协议的典型漏洞——认证漂移问题和DoS攻击.从Attack2、Attack4中发现Woo-lam协议的安全性依赖于参与者的合法身份标识,也即认证中心与参与者之间的对称密钥,但这并不可靠.例如,在Attack4中Malice利用Trent的预言机服务,获得了对Alice的合法身份标识,成功欺骗Bob认证了Alice,而Alice认为他与Bob达到了认证关系.

5 总结

针对协议安全性测试缺乏对安全属性描述及其相关测试方法的问题,本文提出了一种用于检测协议认证安全属性的测试方法.首先建立SPG-EFSM模型,扩展描述目标集合,通过结合参与者目标与协议执行后状态进一步描述认证安全属性.然后,基于SPG-EFSM模型将协议攻击场景分类,以攻击者拥有合法身份、多方参与、多个会话等特殊情况；在此基础上,结合了Dolev-Yao攻击模型,设计了一种包含上述分类的协议认证性攻击算法.通过对Woo-lam协议和μTESLA协议认证性的测试发现,本方法具有可行性、覆盖率高等特点.

[1]周彦伟,杨波,张文政.异构无线网络可控匿名漫游认证协议[J].电子学报,2016,44(5):1117-1123.

ZHOU Yan-wei,YANG Bo,ZHANG Wen-zheng.Controllable and anonymous roaming protocol for heterogeneous wireless network[J].Acta Electronica Sinica,2016,44(5):1117-1123.(in Chinese)

[2]Dalal Alrajeh,Jeff Kramer,Alessandra Russo,et al.Elaborating requirements using model checking and inductive learning [J].IEEE Transactions on Software Engineering,2013,39(3):361-383.

[3]李顺东,杨坤伟,巩林明,等.标准模型下可公开验证的匿名IBE方案[J].电子学报,2016,44(3):673-678.

LI Shun-dong,YANG Kun-wei,GONG Lin-ming,et al.A publicly verifiable anonymous IBE scheme in the standard model[J].Acta Electronica Sinica,2016,44(3):673-678.(in Chinese)

[4]Wen Tang,Sui Ai-Fen,Wolfgang Schmid.A model guided security vulnerability discovery approach for network protocol implementation[A].Proceedings of the 13th International Conference on Communication Technology[C].Beijing,China:IEEE,2011.675-680.

[5]Andrea Arcuri,Muhammad Zohaib Iqbal,Lionel Briand.Random testing:theoretical results and practical implications[J].IEEE Transactions on Software Engineering,2012,38(2):258-277.

[6]G Fraser,A Arcuri.Whole test suite generation[J].IEEE Transactions on Software Engineering,2013,39(2):276-291.

[7]Oulu University Secure Programming Group.PROTOS:Security Testing of Protocol Implementation [OL].http://www.ee.oulu.fi/research/ouspg/protos/index.html,2012-06-12.

[8]Tal O,Knight S,Dean T.Syntax-based vulnerability testing of frame-based network protocols[A]. Proceedings of the 21nd Conference on Privacy,Security and Trust[C].Fredericton:IEEE,2004.13-15.

[9]Jing C,Wang Z,Yin X,et al.Mutation testing of protocol messages based on extended TTCN-3[A].Proceedings of the 22nd International Conference on Advanced Information Networking and Applications[C].Okinawa:IEEE,2008.667-674.

[10]Fabian Yamaguchi,Nico Golde,Daniel Arp,et al.Modeling and discovering vulnerabilities with code property graphs[A].Proceedings of IEEE Symposium on Security and Privacy[C].San Jose:IEEE,2014.590-604.

[11]Gali Mashtizadeh,Andrea Bittau,Dan Boneh,et al.CCFI:cryptographically enforced control flow integrity [A].Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security[C].New York:ACM,2015.941-951.

[12]Shu G,Lee G.Formal methods and tools for testing communication protocol system security[D].Ohio,USA:Ohio State University,2008.

[13]Dolev D,Yao A.On the security of public-key protocols[J].IEEE Transaction on Information Theory,1983,29(2):198-208.

[14]Woo T,Lam S.Authentication for distributed systems[J].ACM Transactions on Computer Systems,1992,25(1):35-39.

[15]Perrig A,Szewczyk R,et al.SPINS:Security protocols for sensor networks [J].Wireless Networks,2002,8(5):521-534.

[16]Wenbo Mao.Modern Cryptography:Theory and Practice[M].New Jersey,USA:Prentice Hall,2004.

何云华 男,1987年出生,湖北荆门人,北方工业大学讲师，西安电子科技大学博士,主要研究方向为协议测试、漏洞挖掘.

E-mail:heyunhua610@163.com

杨 超 男,1979年出生,陕西西安人,西安电子科技大学副教授,主要研究方向为密码学与网络安全,云计算及移动智能计算安全.

E-mail:chaoyang@mail.xidian.edu.cn

Authentication Testing of Security Protocols—A Method for Testing Protocol Security Properties

HE Yun-hua1，2,YANG Chao1,ZHANG Jun-wei1,MA Jian-feng1

(1.KeyLaboratoryofComputerNetworkandInformationSecurityofMinistryofEducation,XidianUniversity,Xi’an,Shaanxi710071,China； 2.DepartmentofInformationSecurity,CollegeofComputerScience,NorthChinaUniversityofTechnology,Beijing100029,China)

Authentication builds the trust relationship between communication parties,which is a magnitude guarantee for secure communications.However,existing protocol testing techniques focus on validating the protocol specification.Those techniques can not satisfy the requirements of testing protocol authentication as their lack of the method for describing security properties.Therefore,a protocol security property testing method is proposed for testing protocol authentication.This testing method uses a new formal model-Symbolic Parameterized Goal Extended Finite State Machine (SPG-EFSM) for describing protocols and their security properties.Then,a protocol attack algorithm is designed for testing protocol authentication based on different attack scenarios.Through test experiments on the well-known protocol Woo-lam and μTESLA,it is found that the SPG-EFSM based attack algorithm can find several protocol security flaws and has better feasibility and high coverage.

protocol testing；security properties；authentication testing；formal model；attack classification

2015-10-27；

2016-05-19；责任编辑：李勇锋

国家自然科学基金青年基金(No.61303219);陕西省自然科学基础研究计划(No.2014JQ8295);中央高校基本科研业务费(No.JB140303);国家自然科学基金面上基金(No.61672415)

TP309

A

0372-2112 (2016)11-2788-08

��学报URL:http://www.ejournal.org.cn

10.3969/j.issn.0372-2112.2016.11.031