賴英旭, 劉 巖, 劉 靜

(北京工業(yè)大學(xué) 信息學(xué)部 計算機學(xué)院,北京 100124)

隨著網(wǎng)絡(luò)技術(shù)和“互聯(lián)網(wǎng)+”應(yīng)用的快速發(fā)展,國民經(jīng)濟和社會發(fā)展越來越依賴基礎(chǔ)網(wǎng)絡(luò)和信息系統(tǒng)[1].國務(wù)院關(guān)于深化“互聯(lián)網(wǎng)+先進(jìn)制造業(yè)”發(fā)展工業(yè)互聯(lián)網(wǎng)的指導(dǎo)意見中明確指出:要完善生態(tài)體系,整合企業(yè)資源,鼓勵企業(yè)跨領(lǐng)域、跨產(chǎn)業(yè)鏈緊密協(xié)作,協(xié)同發(fā)展.在此過程中,網(wǎng)絡(luò)的可信互連是企業(yè)間協(xié)同生產(chǎn)的基礎(chǔ),是保障企業(yè)間共享資源、緊密協(xié)作的重點.網(wǎng)絡(luò)本身具有脆弱性,為保護(hù)網(wǎng)絡(luò)中信息系統(tǒng)的安全,由防火墻、入侵檢測、病毒防范系統(tǒng)等組成的傳統(tǒng)信息安全系統(tǒng)得到廣泛運用.但這些傳統(tǒng)的信息安全系統(tǒng)以抵擋外部入侵為主要手段,很難從源頭上保障信息系統(tǒng)的安全,治標(biāo)不治本[2,3].

可信計算組織(trusted computing group,簡稱TCG)提出了可信網(wǎng)絡(luò)連接(trusted network connection,簡稱TNC)規(guī)范[4,5],在可信計算基礎(chǔ)上,依據(jù)TPM可信度量和報告機制構(gòu)建分層的可信網(wǎng)絡(luò)框架.TNC對終端進(jìn)行用戶認(rèn)證,包括用戶身份的檢查以及平臺認(rèn)證和平臺完整性檢查.TNC采用了VPN和IEEE 802.1x進(jìn)行認(rèn)證并建立通道,將終端的可信狀態(tài)延續(xù)到網(wǎng)絡(luò)中,極大提高了網(wǎng)絡(luò)安全性.然而,TNC只能針對終端進(jìn)行了單向可信認(rèn)證,還存在無法抵御偽裝及重放攻擊等問題[6?11].

針對TNC的不足,我國制定了《信息安全技術(shù) 可信計算規(guī)范 可信連接架構(gòu)》標(biāo)準(zhǔn)[12],該標(biāo)準(zhǔn)采用了一種三元三層、對等、集中管理的可信連接架構(gòu)(trusted connect architecture,簡稱TCA)技術(shù).為了集中管理訪問請求者和訪問控制者,引入了策略管理器作為可信第三方,實現(xiàn)了對訪問請求者和訪問控制者的雙向可信認(rèn)證和評估.然而,面對深化“互聯(lián)網(wǎng)+先進(jìn)制造業(yè)”進(jìn)程中網(wǎng)絡(luò)互連的安全需求,TCA技術(shù)僅提供了終端接入網(wǎng)絡(luò)的可信連接方案,無法適用于網(wǎng)絡(luò)間的可信認(rèn)證.

本文對 TCA進(jìn)行擴展,提出了一種支持網(wǎng)絡(luò)間互連的可信連接協(xié)議 TCA-SNI(TCA-support network interconnection).通過引入網(wǎng)絡(luò)間雙向四元認(rèn)證過程,TCA-SNI具備了網(wǎng)絡(luò)相互評估的機制,增強了TCA在網(wǎng)絡(luò)間的可信認(rèn)證能力.

1 可信連接架構(gòu)

TCA是我國自主創(chuàng)新的一種三元三層的可信連接架構(gòu),在終端連接到網(wǎng)絡(luò)時進(jìn)行雙向身份鑒別和平臺鑒別,實現(xiàn)終端到網(wǎng)絡(luò)的可信連接,其架構(gòu)如圖1所示.

Fig.1 Trusted connect architecture圖1 可信連接架構(gòu)

TCA采用的是三元架構(gòu),存在3個實體[12]:訪問請求者(access requestor,簡稱AR)、訪問控制器(access controller,簡稱AC)和策略管理器(policy manager,簡稱PM).自上至下分為3個抽象層:完整性度量層(integrity measurement layer)、可信平臺評估層(trusted platform evaluation layer)和網(wǎng)絡(luò)訪問層(network access layer).通過身份鑒別、平臺鑒別進(jìn)行訪問控制,身份鑒別可完成身份合法性驗證,平臺鑒別可進(jìn)行平臺完整性評估,從而確保網(wǎng)絡(luò)兩端設(shè)備的可信.TCA支持配置多種平臺完整性評估策略,用戶可針對需要評估的組件設(shè)置靈活或多層次的評估策略,根據(jù)最終的度量結(jié)果,給予不同的訪問權(quán)限.

TCA的具體步驟為[12]:

(1) 在建立可信連接前,TNCC(可信連接客戶端)與TNCAP(可信連接接入點)分別加載它們上層的各個IMC(完整性度量收集者),而EPS(評估策略服務(wù)者)加載它上端的各個IMV(完整性度量校驗者);

(2) NAR(網(wǎng)絡(luò)訪問請求者)向NAC(網(wǎng)絡(luò)訪問控制者)發(fā)起網(wǎng)絡(luò)訪問請求;

(3) NAC收到訪問請求后,與NAR和APS(鑒別策略服務(wù)者)執(zhí)行用戶身份鑒別協(xié)議,來實現(xiàn)AR(訪問請求者)和AC(訪問控制者)之間的雙向用戶身份鑒別.APS在鑒別過程中充當(dāng)可信第三方;

(4) 發(fā)起平臺鑒別過程,NAR向TNCC發(fā)送平臺鑒別請求,NAC向TNCC發(fā)送平臺鑒別請求;

(5) 當(dāng)TNCAP收到平臺鑒別請求時,啟動平臺鑒別過程,與TNCC和EPS執(zhí)行平臺鑒別協(xié)議;

(6) 在平臺鑒別過程中,TNCC通過IF-IMC與其上端的各個IMC進(jìn)行信息交互,TNCAP通過IF-IMC與其上端的各個IMC進(jìn)行信息交互;

(7) EPS負(fù)責(zé)驗證AR和AC的PKI證書,并通過IF-IMV調(diào)用它上端的各個IMV來校驗評估AR和AC的平臺完整性度量值.EPS依據(jù)平臺完整性評估策略生成AR和AC的平臺完整性評估結(jié)果,最后將PKI證書驗證結(jié)果和平臺完整性評估結(jié)果發(fā)送給TNCC和TNCAP;

(8) 當(dāng)AR和AC的平臺鑒別完成時,TNCC和TNCAP分別依據(jù)EPS生成AR和AC的PKI證書驗證結(jié)果和平臺完整性評估結(jié)果生成訪問策略,并分別發(fā)送給NAR和NAC;

(9) NAR依據(jù)它所生成的訪問策略或從TNCC接收到的訪問策略執(zhí)行訪問控制,NAC依據(jù)它所生成的訪問策略或從TNCC接收到的訪問策略執(zhí)行訪問控制,從而實現(xiàn)可信連接.

由上述步驟可以看出,可信連接架構(gòu)與傳統(tǒng)的方法完全不同,可信連接架構(gòu)為網(wǎng)絡(luò)外的用戶或終端規(guī)定了安全策略,只有符合策略的終端才可以接入到網(wǎng)絡(luò)中,將可能導(dǎo)致惡意攻擊的終端隔離到網(wǎng)絡(luò)外,極大地減少了安全隱患.

2 基于TCA的網(wǎng)絡(luò)間可信連接協(xié)議

本文基于TCA技術(shù)的思想,設(shè)計了一種支持網(wǎng)絡(luò)間互連的可信連接協(xié)議TCA-SNI[13],協(xié)議模型如圖2所示.

Fig.2 Trusted connect protocol topology between networks圖2 網(wǎng)絡(luò)間可信連接協(xié)議拓?fù)?/p>

圖2中,每個網(wǎng)絡(luò)中的策略管理器是進(jìn)行可信認(rèn)證的核心設(shè)備,受到高等級保護(hù),僅能與本網(wǎng)中的訪問控制器進(jìn)行通信.訪問請求者在發(fā)起接入網(wǎng)絡(luò)請求時,處于不可信區(qū)域,僅能與訪問控制器通信,在可信認(rèn)證后,才能成功接入網(wǎng)絡(luò),與網(wǎng)絡(luò)內(nèi)除策略管理器外的其他設(shè)備通信.

2.1 設(shè)計思想

2.1.1 網(wǎng)絡(luò)間雙向四元可信認(rèn)證

網(wǎng)絡(luò)1向網(wǎng)絡(luò)2發(fā)送連接請求時,網(wǎng)絡(luò)2的策略管理器為可信第三方,根據(jù)網(wǎng)絡(luò)2的安全策略評估網(wǎng)絡(luò)1的訪問控制器.當(dāng)網(wǎng)絡(luò)2向網(wǎng)絡(luò)1發(fā)送連接請求時,網(wǎng)絡(luò)1的策略管理器為可信第三方,根據(jù)網(wǎng)絡(luò)1的安全策略評估網(wǎng)絡(luò)2的訪問控制器.此雙向四元結(jié)構(gòu)能夠在雙方網(wǎng)絡(luò)安全策略不同的情況下進(jìn)行可信連接,可使兩個網(wǎng)絡(luò)的終端在可信的環(huán)境下進(jìn)行基礎(chǔ)通信.若需要執(zhí)行高級命令,則需繼續(xù)進(jìn)行深度可信認(rèn)證[13].四元三層可信連接架構(gòu)如圖3所示.

Fig.3 Trusted connect architecture between networks圖3 網(wǎng)絡(luò)間可信連接架構(gòu)

2.1.2 多級可信認(rèn)證

網(wǎng)絡(luò)雙方在網(wǎng)間可信連接過程中,不僅對身份信息及完整性信息進(jìn)行可信評估,而且策略管理器還對對方網(wǎng)絡(luò)的安全策略進(jìn)行可信評估.雙方網(wǎng)絡(luò)的策略管理器協(xié)同工作,使網(wǎng)絡(luò)雙方構(gòu)成可信通信環(huán)境.此時,網(wǎng)絡(luò)內(nèi)的終端可以與對方網(wǎng)絡(luò)進(jìn)行基礎(chǔ)通信,完成基本操作.

由于網(wǎng)絡(luò)雙方安全策略的不同,網(wǎng)絡(luò)1中的可信終端可能不符合網(wǎng)絡(luò)2的安全策略,一旦該終端發(fā)送高級控制指令,網(wǎng)絡(luò)2將會面臨安全威脅,造成嚴(yán)重后果.而網(wǎng)絡(luò)1中,只有部分終端需要對網(wǎng)絡(luò)2發(fā)起高級控制指令,因此不需要對網(wǎng)絡(luò)1中所有終端進(jìn)行深度認(rèn)證.對于需要向網(wǎng)絡(luò)2發(fā)送高級命令的終端,應(yīng)進(jìn)行終端深度認(rèn)證.從訪問控制器1到終端逐級進(jìn)行可信認(rèn)證,將完成深度可信認(rèn)證的終端列入網(wǎng)絡(luò)2的白名單,保證安全的同時節(jié)省資源,提高系統(tǒng)運行效率[13].

2.2 協(xié)議工作流程

TCA-SNI協(xié)議有3個階段[13]:終端可信入網(wǎng)、網(wǎng)間可信連接、終端深度認(rèn)證.以圖2中網(wǎng)絡(luò)1與網(wǎng)絡(luò)2可信連接為例,說明此協(xié)議的具體流程.其中,對于身份認(rèn)證,其包括用戶身份和平臺身份的認(rèn)證.用戶身份的驗證可采用靜態(tài)口令、動態(tài)口令、USB KEY、生物特征等多因素身份認(rèn)證方式.平臺身份認(rèn)證可根據(jù)平臺自身的特有標(biāo)識進(jìn)行驗證,如序列號、制造商ID、產(chǎn)品型號、MAC地址等.在本協(xié)議中,可將用戶身份和平臺身份進(jìn)行綁定,共同發(fā)送到策略管理器進(jìn)行認(rèn)證,也可以定制化地接入現(xiàn)有的身份認(rèn)證系統(tǒng).

2.2.1 終端可信入網(wǎng)

本階段是終端可信接入局域網(wǎng)過程[13].使用TPCM引導(dǎo)啟動的終端AR1向AC1發(fā)送接入網(wǎng)絡(luò)請求,AC1接到AR1的請求后,與PM1共同完成與AR1的雙向?qū)Φ瓤尚耪J(rèn)證過程.此過程中,AR1在發(fā)起接入請求時,處于不可信狀態(tài),只能與AC1通信.PM1受到網(wǎng)絡(luò)高安全級別保護(hù),只能與AC1通信,因此AR1與PM1的通信均由AC1轉(zhuǎn)發(fā).具體步驟如下.

其中,CertPM1是PM1的公鑰證書,RandPM1AR1是用來生成PM1與AR1之間通信密鑰的隨機數(shù),RandPM1AC1是用來生成PM1與AC1之間通信密鑰的隨機數(shù).

本階段可信認(rèn)證,可以使網(wǎng)絡(luò)1與網(wǎng)絡(luò)2進(jìn)行正常通信,完成初級命令操作.若部分終端需要進(jìn)行高級操作,則需進(jìn)行終端深度認(rèn)證.

2.2.3 終端深度認(rèn)證

本階段是網(wǎng)絡(luò)1中部分終端向網(wǎng)絡(luò)2發(fā)送高級操作命令前進(jìn)行的深度可信認(rèn)證過程[13].當(dāng)網(wǎng)絡(luò)1中的終端AR1向網(wǎng)絡(luò)2發(fā)送高級操作命令時,需要進(jìn)行深度可信認(rèn)證.該過程由PM2,AC2共同參與,完成對AR1的三元對等認(rèn)證過程.此過程中,PM2受網(wǎng)絡(luò)2的高等級保護(hù),僅能與AC2通信,AR1與PM2的通信由AC2進(jìn)行轉(zhuǎn)發(fā).具體步驟如下.

本階段認(rèn)證,根據(jù)網(wǎng)絡(luò)2的可信評估策略對要進(jìn)行高級命令操作的終端進(jìn)行可信評估,若評估結(jié)果可信,則說明該終端可信,可進(jìn)行高級命令操作.

3 安全性推理及分析

3.1 SVO邏輯

SVO邏輯[14?16]是BAN邏輯的一種擴展,是由Syverson和Orschot在BAN邏輯[17]、GNY邏輯[18]、AT邏輯[19]、VO邏輯[19]等邏輯系統(tǒng)的基礎(chǔ)上提出的,具有以上邏輯的優(yōu)點,同時又具有十分簡潔的推理規(guī)則和公理,是BAN類邏輯中較為成熟的邏輯系統(tǒng).

3.2 SVO邏輯分析協(xié)議

3.2.1 基本語義

SVO邏輯與BAN類邏輯相似,使用符號|≡,?,|～,|≈,|?,?,#,≡分別表示相信(believed)、接收到(reveived)、發(fā)送過(said)、新發(fā)送過(says)、管轄(controls)、擁有(has)、新鮮(fresh)與等價(equivalent)[20].

由規(guī)則R45、規(guī)則R46、規(guī)則R48、公理A1、公理A3可證得協(xié)議目標(biāo)(13)～協(xié)議目標(biāo)(16).

至此,協(xié)議目標(biāo)以全部證出.從上述SVO邏輯分析可以得出,TCA-SNI協(xié)議達(dá)到了網(wǎng)絡(luò)間可信認(rèn)證的目標(biāo),具有較高的安全性.

4 安全性測試及分析

4.1 AVISPA工具

我們選擇Dolev-Yao攻擊者模型[27?30]測試TCA-SNI協(xié)議.在Dolev-Yao模型中,入侵者完全控制通信信道,協(xié)議中消息的傳遞必須經(jīng)過入侵者,入侵者可以非常容易地竊聽、分析、攔截和修改任何消息,可以合法地參與協(xié)議的運行,并向任何人發(fā)送偽造的消息.

AVISPA(automated validation of internet security protocols and applications)[31?34]是一套著名的建立和分析安全協(xié)議模型工具,融合了4種不同的分析工具:動態(tài)模型檢驗期(OFMC)、基于邏輯約束的攻擊搜索器(CLAtSe)、基于SAT的模型檢驗器(SATMC)、基于自動逼近的樹自動機安全協(xié)議分析(TA4SP).AVISPA架構(gòu)如圖4所示.

Fig.4 AVISPA architecture圖4 AVISPA架構(gòu)

AVISPA工具采用HLPSL(high level protocol specification language)[35?37]語言對協(xié)議建立分析模型,通過HLPSL2IF工具轉(zhuǎn)化為IF(intermediate format)語言,在Dolev-Yao安全模型下進(jìn)行分析.AVISPA工具可以直接讀取IF語言,分析協(xié)議是否滿足安全目標(biāo).如果協(xié)議不安全,分析工具將會顯示導(dǎo)致不安全事件發(fā)生的攻擊軌跡.

4.2 實驗過程

4.2.1 基本角色(role)

HLPSL是基于角色的形式化語言.協(xié)議中每個參與者分別定義為一個角色,見表1,分別建立訪問請求者(ar1)、訪問控制器1(ac1)、策略管理器1(pm1)、訪問控制器2(ac2)、策略管理器2(pm2).

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

4.2.2 會話場景

我們定義了4種會話場景來驗證TCA-SNI協(xié)議是否符合安全目標(biāo).首先,我們定義了一個正常的會話過程,其中包含所有合法的角色(場景1).然后,定義了入侵者偽裝訪問請求者(場景2)、訪問控制器1(場景3)或訪問控制器2(場景4)的情況.上述場景的定義見表2,其中,hh,hk表示不同的散列算法.

Table 2 Summary of session configurations表2 場景定義

4.2.3 安全目標(biāo)

為了評估TCA-SNI協(xié)議的安全性,我們需要確定協(xié)議需要達(dá)成的安全目標(biāo).AVISPA提供了不同的關(guān)鍵字表示安全目標(biāo)[13].在本文實驗中,關(guān)鍵字描述如下.

(1) 秘密檢測.消息T是代理A產(chǎn)生的,且是代理A與代理B之間的秘密.如下所示:

其中,t是在定義安全目標(biāo)時使用的標(biāo)識符.

(2) 強認(rèn)證檢測.如下所示,request關(guān)鍵字聲明代理B確實收到了來自代理A的消息T,witness關(guān)鍵字聲明代理A向代理B發(fā)送了消息T.

其中,t是在定義安全目標(biāo)時使用的標(biāo)識符.

為了評估TCA-SNI協(xié)議安全性,我們定義了如下的安全目標(biāo).

(1) 本協(xié)議根據(jù)通信雙方溝通的隨機數(shù),通過散列算法hk生成通信密鑰,只需保證通信雙方掌握的隨機數(shù)一致即可.因此,需要驗證隨機數(shù)使用散列算法hh計算出的散列值是否一致,并且驗證使用公鑰加密傳輸?shù)碾S機數(shù)是否是保密的.HLPSL描述如下:

(2) 本協(xié)議由策略管理器進(jìn)行身份認(rèn)證及平臺完整性評估,返回對應(yīng)的訪問決策,因此需驗證訪問決策被成功地接收,不被攻擊.HLPSL描述如下:

4.2.4 實驗結(jié)果

本文使用HLPSL語言對TCA-SNI協(xié)議過程進(jìn)行了描述,并開源了HLPSL文件:https://git.io/vhvsR.

將HLPSL模型導(dǎo)入AVISPA工具,使用OFMC和CL-AtSe分析工具搜索攻擊.實驗結(jié)果見表3.

根據(jù)表3的結(jié)果,OFMC和AtSe分析工具對TCA-SNI協(xié)議的分析結(jié)果是安全的(SUMMARY:SAFE),而且沒有發(fā)現(xiàn)協(xié)議缺陷.如果檢測到協(xié)議缺陷,“SUMMARY”字段會顯示“UNSAFE”,并在“DETAILS”字段提示“ATTACK_FOUND”.分析過程中,由HLPSL描述轉(zhuǎn)換為IF形式描述保存在“PROTOCOL”字段給出的路徑中文件名為“131539283395812498.if”的文件中.結(jié)果中的“BACKEND”字段給出所用的后端分析工具類型,“STATISTICS”字段顯示了分析工具所執(zhí)行的時間及搜索的節(jié)點數(shù)或狀態(tài)數(shù)量.

Table 3 Summary of test outputs表3 測試結(jié)果摘要

5 總結(jié)

在促進(jìn)大中小企業(yè)融通發(fā)展、深入推進(jìn)“互聯(lián)網(wǎng)+”的進(jìn)程中,對網(wǎng)絡(luò)的可信互連提出了更高的要求.本文基于可信連接架構(gòu)的思想,提出了一種支持網(wǎng)絡(luò)間互連的可信連接協(xié)議(TCA-SNI).本文分析了可信連接架構(gòu),對該架構(gòu)無法適用于網(wǎng)絡(luò)間可信認(rèn)證的不足進(jìn)行了擴展.以TPCM芯片為可信基礎(chǔ),對終端進(jìn)行動態(tài)可信評估,達(dá)到局域網(wǎng)內(nèi)部可信的狀態(tài).根據(jù)網(wǎng)絡(luò)安全策略不同的特點,提出了雙向四元可信認(rèn)證架構(gòu),通過策略管理器的協(xié)同工作,網(wǎng)絡(luò)間構(gòu)成可信通信環(huán)境,可進(jìn)行基礎(chǔ)操作.若外部終端需要向網(wǎng)絡(luò)內(nèi)發(fā)送高級操作命令,則需要進(jìn)行終端深度認(rèn)證,保障終端在進(jìn)行高級操作時可信.

本文對TCA-SNI協(xié)議的工作流程進(jìn)行了詳細(xì)的說明.TCA-SNI協(xié)議需要通過終端可信入網(wǎng)、網(wǎng)間可信連接、終端深度認(rèn)證這3個階段,達(dá)到網(wǎng)絡(luò)可信互連的目標(biāo).可信評估過程主要由通信密鑰協(xié)商、身份認(rèn)證、平臺完整性評估組成.基于安全考慮,發(fā)起連接請求的終端不能與策略管理器直接通信,需要由訪問控制器進(jìn)行轉(zhuǎn)發(fā).為避免數(shù)據(jù)包遭到篡改或丟棄,TCA-SNI采用了確認(rèn)機制,并對邏輯通信通道進(jìn)行加密.在網(wǎng)間可信連接階段后期,策略管理器對網(wǎng)絡(luò)的安全策略進(jìn)行互相評估,在安全策略不同的情況下,使得網(wǎng)間通信環(huán)境可信.

本文針對TCA-SNI協(xié)議的安全性進(jìn)行了分析.使用擴展SVO邏輯對TCA-SNI協(xié)議進(jìn)行形式化描述,提出了協(xié)議安全目標(biāo),使用推理規(guī)則和公理進(jìn)行邏輯分析,證明此協(xié)議理論上有較高的安全性.隨后,對TCA-SNI協(xié)議進(jìn)行了攻擊測試.使用HLPSL描述語言對TCA-SNI進(jìn)行建模,建立基本角色,定義協(xié)議工作場景并設(shè)定安全目標(biāo),導(dǎo)入AVISPA安全協(xié)議分析工具,使用Dolev-Yao攻擊者模型進(jìn)行攻擊測試.測試結(jié)果表明,TCA-SNI不存在協(xié)議缺陷,證明此協(xié)議可以抵御真實網(wǎng)絡(luò)中的攻擊.