基于形式化模型的電力信息審計系統安全協議驗證方法

蘇霞， 張晶晶， 孫靜

(1.國網河北省電力有限公司， 河北,石家莊 050021；2.國網河北服務中心， 河北,石家莊 050000)

0 引言

網絡技術的迅猛發展促使移動支付以及社交網絡各種新型技術相繼出現，有效地促進了信息安全領域的認證技術以及授權技術的發展[1],其中電力信息審計系統安全協議和安全協議驗證得到社會學者的廣泛關注。由于安全協議具有屬性多樣性和邏輯結構復雜等特點[2]，導致安全驗證協議模型的建立以及協議精準描述變得更加困難,因此如何準確、快速地實現安全協議的認證是目前安全領域的一個重要課題。 最近幾年，國內外相關專家針對該方面的內容進行了大量的研究，例如文獻[3]基于Event-B方法，利用VCC等工具建模設計電力信息審計系統安全形式，完成安全協議驗證;文獻[4]通過形式化驗證方法對半量子協議進行建模和驗證。以上兩種方法雖然在現階段取得了較為滿意的研究成果，但是由于未能使用形式化模型，導致安全協議驗證效率降低，安全協議驗證錯誤率和開銷增加。因此，本文在電力信息審計系統中引入了一種形式化的安全協議驗證方法。

1 方法

1.1 形式化建模

面向電力信息審計系統的安全認證協議不僅可以有效地確保用戶信息的私密性[5]，同時也能夠為用戶提供私密的通信機制,其中通信機制主要通過包含屬性的憑證方式實現。

現階段針對認證協議的形式化工作只能利用粗粒度驗證，對電力信息審計系統而言，現有的形式化驗證工作無法滿足其需求。針對以上問題，本文采用形式化的方法，對各實體間的通訊通道和各主體進行了研究,同時對各個實體的屬性、功能以及交互進程進行了全面的分析。

電力信息審計系統的形式化建模是在標識信息的基礎上，用戶主要通過細粒度的方式對消息進行簽名，在整個操作的過程中包含3個不同的主體[6]，各個主體主要具有以下幾方面的功能。

(1) 屬性證書發布機構

該機構負責發布具有權威效應的資格證書，其具體工作內容包括屬性證書的編制與發行。

(2) 證明者

即認證系統的證明者，主要是由主機平臺和可信平臺模型兩個部分組成。

(3) 驗證者

在認證系統中，服務提供者其實是一個認證系統的驗證者，它可以為證明者提供屬性驗證服務，使用一個經過權威認證的公鑰，或由該證明者提供的屬性證書來完成驗證工作。

在面向可選擇性披露的可信屬性認證系統(SDABCS)中包含一組屬性用戶，其中屬性用戶的屬性簽名是通過屬性密鑰獲取的，且屬性簽名可以采用不同的實體進行驗證[7-8]。

SDABCS系統支持如下的安全特征：在已知用戶屬性簽名密鑰以及屬性的情況下，認證機構需要驗證后來使用者上傳的屬性簽名，但不能決定待定密鑰，因此無法判定該簽名來源。

通常情況下，形式化模型可以表示成六元組的形式，即：

SDABCS-M=TE,UTF,C,PAR,ACT,ALG

(1)

式中，SDABCS-M代表模型的名稱,TE代表模型中全部可信實體集合[9],UTF代表模型全部不可信實體集合,C代表模型中全部通道集合,PAR代表模型中全部參數集合,ACT代表模型中全部實體行為集合,ALG代表模型中全部函數集合。

利用圖1給出屬性對應的認證框架。

圖1 基于屬性的認證框架

C的具體表達形式為

C=ISDABCS-M，OSDABCS-M,IOSDABCS-M

(2)

式中，ISDABCS-M代表系統TSA中全部輸入通道集合,OSDABCS-M代表系統TSA中全部輸出通道集合,IOSDABCS-M代表系統TSA中全部輸入輸出通道集合。

PAR對應的表達形式為

PAR=V,CH,ATTR,OTHP

(3)

式中，V代表系統中全部變量,CH代表全部通道的集合,ATTR代表實體所包含的屬性集合,OTHP代表其他參數集。

ACT的表達形式為

ACT=Input,Output,Inside-action

(4)

式中，Input代表系統中全部輸入行為集合,Output代表系統中全部輸出行為集合,Inside-action代表系統中所有內部行為集合[10-11]。

ALG集合主要通過以下算法組成：

ALG=Setup,AKeyGen,ASetup,AArep,AAproof

(5)

式中，Setup代表用于形成公共參數以及屬性權威機構對應的密鑰對,AKeyGen表示密鑰屬性,ASetup代表使用者的屬性簽名,AArep代表請求和發放證書的過程，具體的表達式為

AArep=ASign,VerSign,VerBSign

(6)

式中，ASign代表系統通過屬性密鑰進行劃分,VerSign代表授權部門對證書的簽名進行確認,VerBSign代表授權部門確認使用者的代理簽名[12]。

式(5)中的AAproof代表用戶為驗證者提供屬性證明，并且驗證者對該屬性進行驗證的過程，即：

AAproof=Divatt,Divask,ZeroP,Asign,VerZeroP

(7)

式中，Divatt代表用戶屬性劃分結果,Divask代表使用者通過屬性密鑰完成屬性簽名,ZeroP代表由鑒定人提供的屬性簽名,VerZeroP代表由鑒定人向用戶提供的屬性證明。

SDABCS系統中包含的主要安全特性如下。

(1) 準確性

當系統中參數準確時，采用簽名算法完成簽名驗證。

(2) 屬性隱私性

在屬性證書初步顯示階段，即使系統中的驗證者和各個權威機構存在關聯也無法查看對應的屬性信息。

(3) 不可偽造性

系統中任何人無法對簽名數據進行偽造。

(4) 匿名性

當系統中的用戶進行屬性證書頒發時，主要使用盲化技術完成權威機構簽名，有效保證不同機構之間不存在任何關聯且無法查看自身簽名，實現匿名保護。

不同的協議在不同的安全模型下均存在不同的隱患，為了全面系統的安全性和隱私性，不僅需要獲取攻擊者所具備的能力，同時還需要滿足系統中的安全特征需求。

當用戶和屬性權威機構兩者均處于誠實狀態下時，需要提供符合系統需求的輸出和輸入，確保系統能夠獲取任何期望的正確執行結果。

系統中存在的誠實實體希望能夠在與系統交互的過程中獲取更多有價值的信息，并且結合權威模型的定義完成屬性隱私性和簽名匿名性的設定。

本文建立了一個形式化的電力信息審計系統。在此基礎上，采用SPIN和AVISPA對電力信息審計系統安全協議進行改進。

1.2 電力信息審計系統安全協議驗證

查找電力信息審計系統安全協議中存在的漏洞的操作流程如圖2所示。

首先，為了檢驗電力信息審計系統的安全協議，必須對協議進行行為抽象以及形式化分析，基于時態邏輯屬性，通過轉換器結合安全協議形式化的語言描述各個主體的行為。

安全協議驗證模型的建模過程除了誠實主體建模之外，更加主要的是攻擊者建模，因此使用Doleo—Yao模型構建無法破解協議的密碼算法，其中在知識以及能力方面，攻擊者和合法主體兩者相當，它能夠截獲網絡中所傳送的全部消息，通過Doleo—Yao模型能夠查看全部的消息修改和發送。當確定攻擊者模型后，設參與協議主體的合法者和攻擊者為不同的安全屬性，可以采用模式檢測技術分析不同主體的網絡協議的安全屬性，具體操作步驟如下。

圖2 電力信息審計系統安全協議驗證流程圖

(1) 結合攻擊者模型以及協議運行模式，通過Promela進行建模。

(2) 通過LTL方程對需要驗證的系統性質進行描述。

(3) 將每個實體轉化為模型需要的源代碼，加入指導器模擬的錯誤跟蹤過程，也就是確定了狀態和狀態轉移集合,在建立狀態轉移的過程中[13]下發pan命令，執行驗證代碼，經過權威機構雙向校驗和協議初始形式化分析后，能夠確定安全協議的功能以及相關屬性。過程如下：

① 通過SPIN對系統的性質進行驗證,對應獲取電力信息審計系統中攻擊者相關信息以及系統存在的漏洞;

② 假設性質是假的，通過SPIN形成trail文件能夠準確查找安全協議中存在的攻擊行為，同時準確反映攻擊者的進攻路徑；

③ 假設性質是真的，則結束驗證。

通過上述操作，有效實現電力信息審計系統安全協議驗證。

2 仿真實驗

為了驗證所提基于形式化模型的電力信息審計系統安全協議驗證方法的綜合有效性，仿真測試環境詳見表1。

(1) 安全協議驗證效率

圖3顯示了3種不同安全協議有效性的比較結果。

分析圖3中的實驗數據可知，雖然3種方法的安全協議驗證效率均在90%以上，但是由于所提方法在實際研究的過程中采用形式化模型對電力信息審計系統進行形式化研究，同時有效地改進了安全協議，促使整體的安全協議驗證效率明顯高于文獻[3]方法和文獻[4]方法。

表1 實驗環境

圖3 不同方法的安全協議驗證效率對比結果

(2) 安全協議驗證錯誤率

分別采用3種方法對相同的電力信息審計系統進行安全協議驗證，本試驗以安全協議驗證錯誤率為指標，具體實驗測試結果如表2所示。

表2 不同方法的安全協議驗證錯誤率

分析表2可知，所提方法的安全協議驗證錯誤率最低,文獻[3]方法的安全協議驗證錯誤率次之,文獻[4]方法的安全協議驗證錯誤率最低。由于所提方法采用形式模型對電力信息審計系統進行分析以及形式化研究，有效地簡化了操作流程，同時促使所提方法的安全協議驗證錯誤率得到有效降低。

(3) 安全協議驗證開銷

對電力信息審計系統進行安全協議驗證的過程中會產生一定的費用，但是由于不同方法的驗證過程不同導致開銷也不同。表3為3種方法的安全協議驗證開銷結果。

表3 不同方法的安全協議驗證開銷對比

由表3可知，所提方法的安全協議驗證開銷明顯低于文獻[3]方法和文獻[4]方法。這是因為所提方法中引用了形式化模型，通過形式化模型對電力信息審計系統進行形式化分析，同時進一步對安全協議進行完善，有效地避免了安全協議中存在的漏洞導致開銷增加。

3 總結

本文針對傳統方法存在的問題，結合形式化模型提出一種基于形式化模型的電力信息審計系統安全協議驗證方法。仿真實驗結果表明，所提方法能夠有效地提升安全協議驗證效率，降低安全協議驗證錯誤率和安全協議驗證開銷。由于條件所限，本文尚存缺陷，未來將對以下幾方面進行改進：

(1) 如何更加全面以及準確地對攻擊者進行行為建模，確保攻擊者的行為更加接近真實情況，大幅度增加驗證結果的準確性;

(2) 引入無線傳感器網絡的研究，后續將花費大量的時間和精力對該方面的內容進行研究。