一种网络间可信连接协议∗

赖英旭, 刘 岩, 刘 静

(北京工业大学 信息学部 计算机学院,北京 100124)

随着网络技术和“互联网+”应用的快速发展,国民经济和社会发展越来越依赖基础网络和信息系统[1].国务院关于深化“互联网+先进制造业”发展工业互联网的指导意见中明确指出:要完善生态体系,整合企业资源,鼓励企业跨领域、跨产业链紧密协作,协同发展.在此过程中,网络的可信互连是企业间协同生产的基础,是保障企业间共享资源、紧密协作的重点.网络本身具有脆弱性,为保护网络中信息系统的安全,由防火墙、入侵检测、病毒防范系统等组成的传统信息安全系统得到广泛运用.但这些传统的信息安全系统以抵挡外部入侵为主要手段,很难从源头上保障信息系统的安全,治标不治本[2,3].

可信计算组织(trusted computing group,简称TCG)提出了可信网络连接(trusted network connection,简称TNC)规范[4,5],在可信计算基础上,依据TPM可信度量和报告机制构建分层的可信网络框架.TNC对终端进行用户认证,包括用户身份的检查以及平台认证和平台完整性检查.TNC采用了VPN和IEEE 802.1x进行认证并建立通道,将终端的可信状态延续到网络中,极大提高了网络安全性.然而,TNC只能针对终端进行了单向可信认证,还存在无法抵御伪装及重放攻击等问题[6−11].

针对TNC的不足,我国制定了《信息安全技术 可信计算规范 可信连接架构》标准[12],该标准采用了一种三元三层、对等、集中管理的可信连接架构(trusted connect architecture,简称TCA)技术.为了集中管理访问请求者和访问控制者,引入了策略管理器作为可信第三方,实现了对访问请求者和访问控制者的双向可信认证和评估.然而,面对深化“互联网+先进制造业”进程中网络互连的安全需求,TCA技术仅提供了终端接入网络的可信连接方案,无法适用于网络间的可信认证.

本文对 TCA进行扩展,提出了一种支持网络间互连的可信连接协议 TCA-SNI(TCA-support network interconnection).通过引入网络间双向四元认证过程,TCA-SNI具备了网络相互评估的机制,增强了TCA在网络间的可信认证能力.

1 可信连接架构

TCA是我国自主创新的一种三元三层的可信连接架构,在终端连接到网络时进行双向身份鉴别和平台鉴别,实现终端到网络的可信连接,其架构如图1所示.

Fig.1 Trusted connect architecture图1 可信连接架构

TCA采用的是三元架构,存在3个实体[12]:访问请求者(access requestor,简称AR)、访问控制器(access controller,简称AC)和策略管理器(policy manager,简称PM).自上至下分为3个抽象层:完整性度量层(integrity measurement layer)、可信平台评估层(trusted platform evaluation layer)和网络访问层(network access layer).通过身份鉴别、平台鉴别进行访问控制,身份鉴别可完成身份合法性验证,平台鉴别可进行平台完整性评估,从而确保网络两端设备的可信.TCA支持配置多种平台完整性评估策略,用户可针对需要评估的组件设置灵活或多层次的评估策略,根据最终的度量结果,给予不同的访问权限.

TCA的具体步骤为[12]:

(1) 在建立可信连接前,TNCC(可信连接客户端)与TNCAP(可信连接接入点)分别加载它们上层的各个IMC(完整性度量收集者),而EPS(评估策略服务者)加载它上端的各个IMV(完整性度量校验者);

(2) NAR(网络访问请求者)向NAC(网络访问控制者)发起网络访问请求;

(3) NAC收到访问请求后,与NAR和APS(鉴别策略服务者)执行用户身份鉴别协议,来实现AR(访问请求者)和AC(访问控制者)之间的双向用户身份鉴别.APS在鉴别过程中充当可信第三方;

(4) 发起平台鉴别过程,NAR向TNCC发送平台鉴别请求,NAC向TNCC发送平台鉴别请求;

(5) 当TNCAP收到平台鉴别请求时,启动平台鉴别过程,与TNCC和EPS执行平台鉴别协议;

(6) 在平台鉴别过程中,TNCC通过IF-IMC与其上端的各个IMC进行信息交互,TNCAP通过IF-IMC与其上端的各个IMC进行信息交互;

(7) EPS负责验证AR和AC的PKI证书,并通过IF-IMV调用它上端的各个IMV来校验评估AR和AC的平台完整性度量值.EPS依据平台完整性评估策略生成AR和AC的平台完整性评估结果,最后将PKI证书验证结果和平台完整性评估结果发送给TNCC和TNCAP;

(8) 当AR和AC的平台鉴别完成时,TNCC和TNCAP分别依据EPS生成AR和AC的PKI证书验证结果和平台完整性评估结果生成访问策略,并分别发送给NAR和NAC;

(9) NAR依据它所生成的访问策略或从TNCC接收到的访问策略执行访问控制,NAC依据它所生成的访问策略或从TNCC接收到的访问策略执行访问控制,从而实现可信连接.

由上述步骤可以看出,可信连接架构与传统的方法完全不同,可信连接架构为网络外的用户或终端规定了安全策略,只有符合策略的终端才可以接入到网络中,将可能导致恶意攻击的终端隔离到网络外,极大地减少了安全隐患.

2 基于TCA的网络间可信连接协议

本文基于TCA技术的思想,设计了一种支持网络间互连的可信连接协议TCA-SNI[13],协议模型如图2所示.

Fig.2 Trusted connect protocol topology between networks图2 网络间可信连接协议拓扑

图2中,每个网络中的策略管理器是进行可信认证的核心设备,受到高等级保护,仅能与本网中的访问控制器进行通信.访问请求者在发起接入网络请求时,处于不可信区域,仅能与访问控制器通信,在可信认证后,才能成功接入网络,与网络内除策略管理器外的其他设备通信.

2.1 设计思想

2.1.1 网络间双向四元可信认证

网络1向网络2发送连接请求时,网络2的策略管理器为可信第三方,根据网络2的安全策略评估网络1的访问控制器.当网络2向网络1发送连接请求时,网络1的策略管理器为可信第三方,根据网络1的安全策略评估网络2的访问控制器.此双向四元结构能够在双方网络安全策略不同的情况下进行可信连接,可使两个网络的终端在可信的环境下进行基础通信.若需要执行高级命令,则需继续进行深度可信认证[13].四元三层可信连接架构如图3所示.

Fig.3 Trusted connect architecture between networks图3 网络间可信连接架构

2.1.2 多级可信认证

网络双方在网间可信连接过程中,不仅对身份信息及完整性信息进行可信评估,而且策略管理器还对对方网络的安全策略进行可信评估.双方网络的策略管理器协同工作,使网络双方构成可信通信环境.此时,网络内的终端可以与对方网络进行基础通信,完成基本操作.

由于网络双方安全策略的不同,网络1中的可信终端可能不符合网络2的安全策略,一旦该终端发送高级控制指令,网络2将会面临安全威胁,造成严重后果.而网络1中,只有部分终端需要对网络2发起高级控制指令,因此不需要对网络1中所有终端进行深度认证.对于需要向网络2发送高级命令的终端,应进行终端深度认证.从访问控制器1到终端逐级进行可信认证,将完成深度可信认证的终端列入网络2的白名单,保证安全的同时节省资源,提高系统运行效率[13].

2.2 协议工作流程

TCA-SNI协议有3个阶段[13]:终端可信入网、网间可信连接、终端深度认证.以图2中网络1与网络2可信连接为例,说明此协议的具体流程.其中,对于身份认证,其包括用户身份和平台身份的认证.用户身份的验证可采用静态口令、动态口令、USB KEY、生物特征等多因素身份认证方式.平台身份认证可根据平台自身的特有标识进行验证,如序列号、制造商ID、产品型号、MAC地址等.在本协议中,可将用户身份和平台身份进行绑定,共同发送到策略管理器进行认证,也可以定制化地接入现有的身份认证系统.

2.2.1 终端可信入网

本阶段是终端可信接入局域网过程[13].使用TPCM引导启动的终端AR1向AC1发送接入网络请求,AC1接到AR1的请求后,与PM1共同完成与AR1的双向对等可信认证过程.此过程中,AR1在发起接入请求时,处于不可信状态,只能与AC1通信.PM1受到网络高安全级别保护,只能与AC1通信,因此AR1与PM1的通信均由AC1转发.具体步骤如下.

其中,CertPM1是PM1的公钥证书,RandPM1AR1是用来生成PM1与AR1之间通信密钥的随机数,RandPM1AC1是用来生成PM1与AC1之间通信密钥的随机数.

本阶段可信认证,可以使网络1与网络2进行正常通信,完成初级命令操作.若部分终端需要进行高级操作,则需进行终端深度认证.

2.2.3 终端深度认证

本阶段是网络1中部分终端向网络2发送高级操作命令前进行的深度可信认证过程[13].当网络1中的终端AR1向网络2发送高级操作命令时,需要进行深度可信认证.该过程由PM2,AC2共同参与,完成对AR1的三元对等认证过程.此过程中,PM2受网络2的高等级保护,仅能与AC2通信,AR1与PM2的通信由AC2进行转发.具体步骤如下.

本阶段认证,根据网络2的可信评估策略对要进行高级命令操作的终端进行可信评估,若评估结果可信,则说明该终端可信,可进行高级命令操作.

3 安全性推理及分析

3.1 SVO逻辑

SVO逻辑[14−16]是BAN逻辑的一种扩展,是由Syverson和Orschot在BAN逻辑[17]、GNY逻辑[18]、AT逻辑[19]、VO逻辑[19]等逻辑系统的基础上提出的,具有以上逻辑的优点,同时又具有十分简洁的推理规则和公理,是BAN类逻辑中较为成熟的逻辑系统.

3.2 SVO逻辑分析协议

3.2.1 基本语义

SVO逻辑与BAN类逻辑相似,使用符号|≡,◁,|～,|≈,|⇒,∋,#,≡分别表示相信(believed)、接收到(reveived)、发送过(said)、新发送过(says)、管辖(controls)、拥有(has)、新鲜(fresh)与等价(equivalent)[20].

由规则R45、规则R46、规则R48、公理A1、公理A3可证得协议目标(13)～协议目标(16).

至此,协议目标以全部证出.从上述SVO逻辑分析可以得出,TCA-SNI协议达到了网络间可信认证的目标,具有较高的安全性.

4 安全性测试及分析

4.1 AVISPA工具

我们选择Dolev-Yao攻击者模型[27−30]测试TCA-SNI协议.在Dolev-Yao模型中,入侵者完全控制通信信道,协议中消息的传递必须经过入侵者,入侵者可以非常容易地窃听、分析、拦截和修改任何消息,可以合法地参与协议的运行,并向任何人发送伪造的消息.

AVISPA(automated validation of internet security protocols and applications)[31−34]是一套著名的建立和分析安全协议模型工具,融合了4种不同的分析工具:动态模型检验期(OFMC)、基于逻辑约束的攻击搜索器(CLAtSe)、基于SAT的模型检验器(SATMC)、基于自动逼近的树自动机安全协议分析(TA4SP).AVISPA架构如图4所示.

Fig.4 AVISPA architecture图4 AVISPA架构

AVISPA工具采用HLPSL(high level protocol specification language)[35−37]语言对协议建立分析模型,通过HLPSL2IF工具转化为IF(intermediate format)语言,在Dolev-Yao安全模型下进行分析.AVISPA工具可以直接读取IF语言,分析协议是否满足安全目标.如果协议不安全,分析工具将会显示导致不安全事件发生的攻击轨迹.

4.2 实验过程

4.2.1 基本角色(role)

HLPSL是基于角色的形式化语言.协议中每个参与者分别定义为一个角色,见表1,分别建立访问请求者(ar1)、访问控制器1(ac1)、策略管理器1(pm1)、访问控制器2(ac2)、策略管理器2(pm2).

Table 1 Definition of the basic roles表1 基本角色定义

4.2.2 会话场景

我们定义了4种会话场景来验证TCA-SNI协议是否符合安全目标.首先,我们定义了一个正常的会话过程,其中包含所有合法的角色(场景1).然后,定义了入侵者伪装访问请求者(场景2)、访问控制器1(场景3)或访问控制器2(场景4)的情况.上述场景的定义见表2,其中,hh,hk表示不同的散列算法.

Table 2 Summary of session configurations表2 场景定义

4.2.3 安全目标

为了评估TCA-SNI协议的安全性,我们需要确定协议需要达成的安全目标.AVISPA提供了不同的关键字表示安全目标[13].在本文实验中,关键字描述如下.

(1) 秘密检测.消息T是代理A产生的,且是代理A与代理B之间的秘密.如下所示:

其中,t是在定义安全目标时使用的标识符.

(2) 强认证检测.如下所示,request关键字声明代理B确实收到了来自代理A的消息T,witness关键字声明代理A向代理B发送了消息T.

其中,t是在定义安全目标时使用的标识符.

为了评估TCA-SNI协议安全性,我们定义了如下的安全目标.

(1) 本协议根据通信双方沟通的随机数,通过散列算法hk生成通信密钥,只需保证通信双方掌握的随机数一致即可.因此,需要验证随机数使用散列算法hh计算出的散列值是否一致,并且验证使用公钥加密传输的随机数是否是保密的.HLPSL描述如下:

(2) 本协议由策略管理器进行身份认证及平台完整性评估,返回对应的访问决策,因此需验证访问决策被成功地接收,不被攻击.HLPSL描述如下:

4.2.4 实验结果

本文使用HLPSL语言对TCA-SNI协议过程进行了描述,并开源了HLPSL文件:https://git.io/vhvsR.

将HLPSL模型导入AVISPA工具,使用OFMC和CL-AtSe分析工具搜索攻击.实验结果见表3.

根据表3的结果,OFMC和AtSe分析工具对TCA-SNI协议的分析结果是安全的(SUMMARY:SAFE),而且没有发现协议缺陷.如果检测到协议缺陷,“SUMMARY”字段会显示“UNSAFE”,并在“DETAILS”字段提示“ATTACK_FOUND”.分析过程中,由HLPSL描述转换为IF形式描述保存在“PROTOCOL”字段给出的路径中文件名为“131539283395812498.if”的文件中.结果中的“BACKEND”字段给出所用的后端分析工具类型,“STATISTICS”字段显示了分析工具所执行的时间及搜索的节点数或状态数量.

Table 3 Summary of test outputs表3 测试结果摘要

5 总结

在促进大中小企业融通发展、深入推进“互联网+”的进程中,对网络的可信互连提出了更高的要求.本文基于可信连接架构的思想,提出了一种支持网络间互连的可信连接协议(TCA-SNI).本文分析了可信连接架构,对该架构无法适用于网络间可信认证的不足进行了扩展.以TPCM芯片为可信基础,对终端进行动态可信评估,达到局域网内部可信的状态.根据网络安全策略不同的特点,提出了双向四元可信认证架构,通过策略管理器的协同工作,网络间构成可信通信环境,可进行基础操作.若外部终端需要向网络内发送高级操作命令,则需要进行终端深度认证,保障终端在进行高级操作时可信.

本文对TCA-SNI协议的工作流程进行了详细的说明.TCA-SNI协议需要通过终端可信入网、网间可信连接、终端深度认证这3个阶段,达到网络可信互连的目标.可信评估过程主要由通信密钥协商、身份认证、平台完整性评估组成.基于安全考虑,发起连接请求的终端不能与策略管理器直接通信,需要由访问控制器进行转发.为避免数据包遭到篡改或丢弃,TCA-SNI采用了确认机制,并对逻辑通信通道进行加密.在网间可信连接阶段后期,策略管理器对网络的安全策略进行互相评估,在安全策略不同的情况下,使得网间通信环境可信.

本文针对TCA-SNI协议的安全性进行了分析.使用扩展SVO逻辑对TCA-SNI协议进行形式化描述,提出了协议安全目标,使用推理规则和公理进行逻辑分析,证明此协议理论上有较高的安全性.随后,对TCA-SNI协议进行了攻击测试.使用HLPSL描述语言对TCA-SNI进行建模,建立基本角色,定义协议工作场景并设定安全目标,导入AVISPA安全协议分析工具,使用Dolev-Yao攻击者模型进行攻击测试.测试结果表明,TCA-SNI不存在协议缺陷,证明此协议可以抵御真实网络中的攻击.