基于形式化模型的電力信息審計(jì)系統(tǒng)安全協(xié)議驗(yàn)證方法

蘇霞， 張晶晶， 孫靜

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

0 引言

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

1 方法

1.1 形式化建模

面向電力信息審計(jì)系統(tǒng)的安全認(rèn)證協(xié)議不僅可以有效地確保用戶信息的私密性[5]，同時(shí)也能夠?yàn)橛脩籼峁┧矫艿耐ㄐ艡C(jī)制,其中通信機(jī)制主要通過包含屬性的憑證方式實(shí)現(xiàn)。

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

電力信息審計(jì)系統(tǒng)的形式化建模是在標(biāo)識(shí)信息的基礎(chǔ)上，用戶主要通過細(xì)粒度的方式對(duì)消息進(jìn)行簽名，在整個(gè)操作的過程中包含3個(gè)不同的主體[6]，各個(gè)主體主要具有以下幾方面的功能。

(1) 屬性證書發(fā)布機(jī)構(gòu)

該機(jī)構(gòu)負(fù)責(zé)發(fā)布具有權(quán)威效應(yīng)的資格證書，其具體工作內(nèi)容包括屬性證書的編制與發(fā)行。

(2) 證明者

即認(rèn)證系統(tǒng)的證明者，主要是由主機(jī)平臺(tái)和可信平臺(tái)模型兩個(gè)部分組成。

(3) 驗(yàn)證者

在認(rèn)證系統(tǒng)中，服務(wù)提供者其實(shí)是一個(gè)認(rèn)證系統(tǒng)的驗(yàn)證者，它可以為證明者提供屬性驗(yàn)證服務(wù)，使用一個(gè)經(jīng)過權(quán)威認(rèn)證的公鑰，或由該證明者提供的屬性證書來完成驗(yàn)證工作。

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

SDABCS系統(tǒng)支持如下的安全特征：在已知用戶屬性簽名密鑰以及屬性的情況下，認(rèn)證機(jī)構(gòu)需要驗(yàn)證后來使用者上傳的屬性簽名，但不能決定待定密鑰，因此無法判定該簽名來源。

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

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

(1)

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

利用圖1給出屬性對(duì)應(yīng)的認(rèn)證框架。

圖1 基于屬性的認(rèn)證框架

C的具體表達(dá)形式為

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

(2)

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

PAR對(duì)應(yīng)的表達(dá)形式為

PAR=V,CH,ATTR,OTHP

(3)

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

ACT的表達(dá)形式為

ACT=Input,Output,Inside-action

(4)

式中，Input代表系統(tǒng)中全部輸入行為集合,Output代表系統(tǒng)中全部輸出行為集合,Inside-action代表系統(tǒng)中所有內(nèi)部行為集合[10-11]。

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

ALG=Setup,AKeyGen,ASetup,AArep,AAproof

(5)

式中，Setup代表用于形成公共參數(shù)以及屬性權(quán)威機(jī)構(gòu)對(duì)應(yīng)的密鑰對(duì),AKeyGen表示密鑰屬性,ASetup代表使用者的屬性簽名,AArep代表請(qǐng)求和發(fā)放證書的過程，具體的表達(dá)式為

AArep=ASign,VerSign,VerBSign

(6)

式中，ASign代表系統(tǒng)通過屬性密鑰進(jìn)行劃分,VerSign代表授權(quán)部門對(duì)證書的簽名進(jìn)行確認(rèn),VerBSign代表授權(quán)部門確認(rèn)使用者的代理簽名[12]。

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

AAproof=Divatt,Divask,ZeroP,Asign,VerZeroP

(7)

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

SDABCS系統(tǒng)中包含的主要安全特性如下。

(1) 準(zhǔn)確性

當(dāng)系統(tǒng)中參數(shù)準(zhǔn)確時(shí)，采用簽名算法完成簽名驗(yàn)證。

(2) 屬性隱私性

在屬性證書初步顯示階段，即使系統(tǒng)中的驗(yàn)證者和各個(gè)權(quán)威機(jī)構(gòu)存在關(guān)聯(lián)也無法查看對(duì)應(yīng)的屬性信息。

(3) 不可偽造性

系統(tǒng)中任何人無法對(duì)簽名數(shù)據(jù)進(jìn)行偽造。

(4) 匿名性

當(dāng)系統(tǒng)中的用戶進(jìn)行屬性證書頒發(fā)時(shí)，主要使用盲化技術(shù)完成權(quán)威機(jī)構(gòu)簽名，有效保證不同機(jī)構(gòu)之間不存在任何關(guān)聯(lián)且無法查看自身簽名，實(shí)現(xiàn)匿名保護(hù)。

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

當(dāng)用戶和屬性權(quán)威機(jī)構(gòu)兩者均處于誠(chéng)實(shí)狀態(tài)下時(shí)，需要提供符合系統(tǒng)需求的輸出和輸入，確保系統(tǒng)能夠獲取任何期望的正確執(zhí)行結(jié)果。

系統(tǒng)中存在的誠(chéng)實(shí)實(shí)體希望能夠在與系統(tǒng)交互的過程中獲取更多有價(jià)值的信息，并且結(jié)合權(quán)威模型的定義完成屬性隱私性和簽名匿名性的設(shè)定。

本文建立了一個(gè)形式化的電力信息審計(jì)系統(tǒng)。在此基礎(chǔ)上，采用SPIN和AVISPA對(duì)電力信息審計(jì)系統(tǒng)安全協(xié)議進(jìn)行改進(jìn)。

1.2 電力信息審計(jì)系統(tǒng)安全協(xié)議驗(yàn)證

查找電力信息審計(jì)系統(tǒng)安全協(xié)議中存在的漏洞的操作流程如圖2所示。

首先，為了檢驗(yàn)電力信息審計(jì)系統(tǒng)的安全協(xié)議，必須對(duì)協(xié)議進(jìn)行行為抽象以及形式化分析，基于時(shí)態(tài)邏輯屬性，通過轉(zhuǎn)換器結(jié)合安全協(xié)議形式化的語言描述各個(gè)主體的行為。

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

圖2 電力信息審計(jì)系統(tǒng)安全協(xié)議驗(yàn)證流程圖

(1) 結(jié)合攻擊者模型以及協(xié)議運(yùn)行模式，通過Promela進(jìn)行建模。

(2) 通過LTL方程對(duì)需要驗(yàn)證的系統(tǒng)性質(zhì)進(jìn)行描述。

(3) 將每個(gè)實(shí)體轉(zhuǎn)化為模型需要的源代碼，加入指導(dǎo)器模擬的錯(cuò)誤跟蹤過程，也就是確定了狀態(tài)和狀態(tài)轉(zhuǎn)移集合,在建立狀態(tài)轉(zhuǎn)移的過程中[13]下發(fā)pan命令，執(zhí)行驗(yàn)證代碼，經(jīng)過權(quán)威機(jī)構(gòu)雙向校驗(yàn)和協(xié)議初始形式化分析后，能夠確定安全協(xié)議的功能以及相關(guān)屬性。過程如下：

① 通過SPIN對(duì)系統(tǒng)的性質(zhì)進(jìn)行驗(yàn)證,對(duì)應(yīng)獲取電力信息審計(jì)系統(tǒng)中攻擊者相關(guān)信息以及系統(tǒng)存在的漏洞;

② 假設(shè)性質(zhì)是假的，通過SPIN形成trail文件能夠準(zhǔn)確查找安全協(xié)議中存在的攻擊行為，同時(shí)準(zhǔn)確反映攻擊者的進(jìn)攻路徑；

③ 假設(shè)性質(zhì)是真的，則結(jié)束驗(yàn)證。

通過上述操作，有效實(shí)現(xiàn)電力信息審計(jì)系統(tǒng)安全協(xié)議驗(yàn)證。

2 仿真實(shí)驗(yàn)

為了驗(yàn)證所提基于形式化模型的電力信息審計(jì)系統(tǒng)安全協(xié)議驗(yàn)證方法的綜合有效性，仿真測(cè)試環(huán)境詳見表1。

(1) 安全協(xié)議驗(yàn)證效率

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

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

表1 實(shí)驗(yàn)環(huán)境

圖3 不同方法的安全協(xié)議驗(yàn)證效率對(duì)比結(jié)果

(2) 安全協(xié)議驗(yàn)證錯(cuò)誤率

分別采用3種方法對(duì)相同的電力信息審計(jì)系統(tǒng)進(jìn)行安全協(xié)議驗(yàn)證，本試驗(yàn)以安全協(xié)議驗(yàn)證錯(cuò)誤率為指標(biāo)，具體實(shí)驗(yàn)測(cè)試結(jié)果如表2所示。

表2 不同方法的安全協(xié)議驗(yàn)證錯(cuò)誤率

分析表2可知，所提方法的安全協(xié)議驗(yàn)證錯(cuò)誤率最低,文獻(xiàn)[3]方法的安全協(xié)議驗(yàn)證錯(cuò)誤率次之,文獻(xiàn)[4]方法的安全協(xié)議驗(yàn)證錯(cuò)誤率最低。由于所提方法采用形式模型對(duì)電力信息審計(jì)系統(tǒng)進(jìn)行分析以及形式化研究，有效地簡(jiǎn)化了操作流程，同時(shí)促使所提方法的安全協(xié)議驗(yàn)證錯(cuò)誤率得到有效降低。

(3) 安全協(xié)議驗(yàn)證開銷

對(duì)電力信息審計(jì)系統(tǒng)進(jìn)行安全協(xié)議驗(yàn)證的過程中會(huì)產(chǎn)生一定的費(fèi)用，但是由于不同方法的驗(yàn)證過程不同導(dǎo)致開銷也不同。表3為3種方法的安全協(xié)議驗(yàn)證開銷結(jié)果。

表3 不同方法的安全協(xié)議驗(yàn)證開銷對(duì)比

由表3可知，所提方法的安全協(xié)議驗(yàn)證開銷明顯低于文獻(xiàn)[3]方法和文獻(xiàn)[4]方法。這是因?yàn)樗岱椒ㄖ幸昧诵问交Ｐ停ㄟ^形式化模型對(duì)電力信息審計(jì)系統(tǒng)進(jìn)行形式化分析，同時(shí)進(jìn)一步對(duì)安全協(xié)議進(jìn)行完善，有效地避免了安全協(xié)議中存在的漏洞導(dǎo)致開銷增加。

3 總結(jié)

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

(1) 如何更加全面以及準(zhǔn)確地對(duì)攻擊者進(jìn)行行為建模，確保攻擊者的行為更加接近真實(shí)情況，大幅度增加驗(yàn)證結(jié)果的準(zhǔn)確性;

(2) 引入無線傳感器網(wǎng)絡(luò)的研究，后續(xù)將花費(fèi)大量的時(shí)間和精力對(duì)該方面的內(nèi)容進(jìn)行研究。