一種網絡間可信連接協議?

賴英旭, 劉 巖, 劉 靜

(北京工業大學 信息學部 計算機學院,北京 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不存在協議缺陷,證明此協議可以抵御真實網絡中的攻擊.