基于PAT的使用控制模型的形式化規(guī)約與安全性分析

周從華，陳偉鶴，劉志鋒

（江蘇大學(xué)計(jì)算機(jī)科學(xué)與通信工程學(xué)院，江蘇 鎮(zhèn)江 212013）

基于PAT的使用控制模型的形式化規(guī)約與安全性分析

周從華，陳偉鶴，劉志鋒

（江蘇大學(xué)計(jì)算機(jī)科學(xué)與通信工程學(xué)院，江蘇 鎮(zhèn)江 212013）

使用控制模型UCON是高度分布式、網(wǎng)絡(luò)化的異構(gòu)開放式計(jì)算環(huán)境下實(shí)現(xiàn)數(shù)字資源保護(hù)的新型訪問控制模型。首先，利用態(tài)式時間進(jìn)程代數(shù) TCSP#建立了每個 UCON核模型的形式化規(guī)約，以及針對一般化UCON的組合規(guī)約機(jī)制。其次，提出了各種基于單會話的進(jìn)程組合機(jī)制，實(shí)現(xiàn)了復(fù)雜并發(fā)會話、時間控制與非確定性的形式化規(guī)范，從而使組合進(jìn)程的可達(dá)空間即為所求空間。最后，提出了基于可達(dá)空間的UCON安全性分析方法，以及基于進(jìn)程代數(shù)等價的控制規(guī)則沖突性分析方法。所有的工作都已在PAT上實(shí)現(xiàn)，表明所提方法是切實(shí)可行的，同時也為UCON的形式化規(guī)范與安全性驗(yàn)證尋找到了一個合適的工具。

UCON；形式化規(guī)約；安全性分析；模型檢測

UCON模型區(qū)別于傳統(tǒng)訪問控制模型的主要特征在于可變屬性與連續(xù)的訪問控制。UCON定義了授權(quán)、義務(wù)和條件3個訪問控制決策因素，必須當(dāng)3個因素都被滿足時訪問才能得到許可。在UCON中，決策因素并不僅僅在訪問執(zhí)行之前被檢測，在訪問的過程中亦會被重復(fù)檢測，只有在訪問過程中主客體屬性的變異和運(yùn)行環(huán)境的變化沒有導(dǎo)致某些決策因素不被滿足時，訪問才可以繼續(xù)，否則撤銷本次訪問。UCON模型不僅包含了DAC、MAC和RBAC，還包含了數(shù)字版權(quán)管理與信任管理等，涵蓋了現(xiàn)代電子商務(wù)和信息系統(tǒng)面臨的安全和隱私 2個重要的信息安全問題。因此，UCON模型為無處不在的計(jì)算環(huán)境下信息的合法訪問提供了一種新方法，被稱作下一代訪問控制模型。

一個正確的訪問控制策略首先應(yīng)該為用戶提供充分的許可來執(zhí)行他們的操作并獲取合法信息，同時應(yīng)該阻止用戶惡意的行為。為了保證控制策略的正確性，控制策略的形式化規(guī)約與安全驗(yàn)證必不可少。規(guī)約可以幫助人們識別可能的系統(tǒng)行為，驗(yàn)證可以幫助人們驗(yàn)證安全性問題，如某個主體最終能否獲得某個客體的訪問權(quán)限。UCON支持可變屬性和連續(xù)決策，這為UCON的形式化規(guī)約與安全性驗(yàn)證帶來了很大挑戰(zhàn)。本文的研究動機(jī)主要在于應(yīng)對此挑戰(zhàn)，從規(guī)約到驗(yàn)證提供一個系統(tǒng)的解決方案，同時尋求現(xiàn)有成熟工具的支持，使方案變得切實(shí)可行。

目前，已有的UCON形式化規(guī)約方式可以分為基于邏輯的形式化規(guī)約［5～7］與基于進(jìn)程代數(shù)的形式化規(guī)約［8，9］。文獻(xiàn)［10］對所有的規(guī)約形式從表達(dá)力方面進(jìn)行了系統(tǒng)的比較，認(rèn)為目前已有的規(guī)約形式在表達(dá)力上有很大欠缺，特別是在并發(fā)使用會話之間的交互、時間控制與非確定性3個方面沒有得到充分的表達(dá)。在UCON的安全性驗(yàn)證上，目前存在的工作比較少。文獻(xiàn)［11］證明了在屬性值域是有限的前提下，僅僅考慮授權(quán)因素的UCON子模型UCONA的安全性是可判定的，但是并沒有給出具體的方法來計(jì)算可達(dá)空間。文獻(xiàn)［12］利用模型檢測工具SPIN［13］對UCON在應(yīng)用層的并發(fā)執(zhí)行進(jìn)行了建模與驗(yàn)證，其考慮的并發(fā)場景僅僅限于主體對客體的單次訪問。

PAT［14］是目前先進(jìn)的模型檢測工具，主要優(yōu)點(diǎn)包括：1）PAT的建模語言TCSP#［15］集成了高層規(guī)約和程序級規(guī)約，支持各種組合操作、實(shí)時性與自定義數(shù)據(jù)結(jié)構(gòu)，具有表達(dá)力強(qiáng)、建模直觀與便捷等特性；2）PAT支持多種性質(zhì)的驗(yàn)證，比如死鎖、可達(dá)性、線性時態(tài)邏輯LTL［16］以及精化。鑒于PAT是一款出色的模型檢測工具，本文的主要研究動機(jī)在于基于PAT平臺，從訪問控制策略的規(guī)約到安全性驗(yàn)證形成一套系統(tǒng)的方法，具體工作包括以下幾個方面：首先，為每個UCON核模型建立TCSP#規(guī)范，為一般化UCON建立規(guī)范組合機(jī)制，使對任意UCON按照這套機(jī)制可完整正確地建立其TCSP#規(guī)范；其次，提出了各種基于單使用會話的進(jìn)程組合機(jī)制，建立了并發(fā)使用會話、時間控制與非確定性的形式化規(guī)范，以此實(shí)現(xiàn)了任意時刻任意主體對任意客體發(fā)起任意訪問請求的形式化規(guī)范以及可達(dá)空間的計(jì)算；最后，提出了基于可達(dá)空間的簡單安全性、簡單可用性等屬性的分析方法，以及基于進(jìn)程代數(shù)等價的控制策略沖突性分析方法。

2　使用控制UCON

UCON支持豐富、細(xì)粒度和持續(xù)的數(shù)字資源的訪問控制。對于許多應(yīng)用如GRID、Web Service、云計(jì)算、無線自組網(wǎng)等UCON均提供了可行的、徹底的解決方案。UCON共由6個部分組成：主體及其屬性、客體及其屬性、權(quán)限、授權(quán)、義務(wù)和條件，其中，授權(quán)、義務(wù)和條件是訪問許可決策模塊。

主體是資源訪問的請求者，能夠激活訪問，同時會采取某些事件來完成訪問。主體主要通過其屬性來定義和表示，主體的屬性是指那些能夠進(jìn)行決策的性質(zhì)或者能力?？腕w是被主體執(zhí)行訪問權(quán)限的實(shí)體，客體的屬性包括那些能夠進(jìn)行決策的性質(zhì)或者能力。權(quán)限與傳統(tǒng)訪問控制中的訪問權(quán)限一致，即表示那些能夠被主客體利用的使用許可。

授權(quán)是定義在主客體屬性上的謂詞，是關(guān)于主客體屬性的約束（如主體的角色必須為主治醫(yī)生），謂詞必須為真訪問請求才可能得到許可。實(shí)際上從傳統(tǒng)的訪問控制系統(tǒng)開始，授權(quán)已經(jīng)獲得了廣泛的應(yīng)用。只不過在UCON中授權(quán)謂詞可能在訪問之前、訪問的過程中進(jìn)行評估，而傳統(tǒng)訪問控制只支持訪問之前的評估。

義務(wù)是主體在訪問客體之前、過程中必須完成的事件（如用戶在注冊前必須簽署遵守某種約定的協(xié)議），增強(qiáng)了UCON模型的表達(dá)力。條件是對系統(tǒng)運(yùn)行環(huán)境的約束，與主客體屬性無關(guān)（如對客體的訪問時間只能限于白天工作時間）。條件謂詞的評估可以在訪問實(shí)施之前或者在訪問實(shí)施過程中執(zhí)行。需要特別注意的是條件檢測不能改變主體、客體和運(yùn)行環(huán)境的屬性。

在UCON中單次使用會話的基本過程可以總結(jié)如下。開始時主體s通過執(zhí)行事件tryaccess.s.o.r發(fā)出對客體o執(zhí)行權(quán)限為r的訪問請求。系統(tǒng)評估授權(quán)謂詞的真值，如果值為假，則立即通過執(zhí)行事件denyaccess.s.o.r來拒絕此次訪問請求，如果值為真，則執(zhí)行事件permitaccess.s.o.r來同意此次訪問請求，并繼續(xù)執(zhí)行事件preupdate.s.o.r來更新屬性的值，執(zhí)行事件doaccess.s.o.r完成訪問請求，系統(tǒng)也進(jìn)入在線使用控制的階段。在訪問過程中，主客體屬性可能需要周期性更新，執(zhí)行事件onupdate.s.o.r來完成該更新過程。在訪問過程中，如果授權(quán)、條件和義務(wù)有一個失效，則系統(tǒng)立即通過執(zhí)行事件revokeaccss.s.o.r來終止此次訪問。在訪問過程中，如果主體主動終止訪問過程，可通過執(zhí)行事件endaccess.s.o.r來實(shí)現(xiàn)。無論是主動終止還是失效終止，終止后屬性的值都可能被更新，這種更新通過事件postupdate.s.o.r來執(zhí)行。需要注意的是，主動終止與失效終止所引起的屬性的變化可能會有所不同。

3　UCON的TCSP#規(guī)范

依據(jù)無處不在計(jì)算環(huán)境下訪問控制的執(zhí)行流程，可以定義如下9個原子事件。

1）tryaccess.s.o.r：主體s對客體o產(chǎn)生一個權(quán)限為r的訪問請求。

2）permitaccess.s.o.r：訪問請求tryaccess.s.o.r得到系統(tǒng)許可。

3）denyaccess.s.o.r：訪問請求 tryaccess.s.o.r被系統(tǒng)拒絕。

4）doaccess.s.o.r：主體s對客體o執(zhí)行權(quán)限為r的訪問。

5）revokeaccess.s.o.r：系統(tǒng)撤銷主體s對客體o正在執(zhí)行的權(quán)限為r的訪問。

6）endaccess.s.o.r：主體s主動結(jié)束對客體o的權(quán)限為r的訪問。

7）preupdate.s.o.r：在訪問被許可前對主客體的屬性進(jìn)行更新，或者在許可被拒絕后對主客體的屬性進(jìn)行更新。

8）onupdate.s.o.r：在訪問的過程中由系統(tǒng)來更新主客體的屬性，這種更新操作在訪問過程中可以重復(fù)進(jìn)行。

9）postupdate.s.o.r：在訪問結(jié)束后由系統(tǒng)更新主客體的屬性。

3.1授權(quán)核模型的規(guī)約

依據(jù)屬性更新的時機(jī)不同，對UCON中的每一個決策構(gòu)件定義了多種核模型，本節(jié)主要討論授權(quán)核模型的 TCSP#規(guī)范。在授權(quán)核模型中，使用控制的決策依賴于主客體的屬性值。依據(jù)屬性更新操作的時間點(diǎn)，即執(zhí)行訪問前、執(zhí)行訪問過程中和訪問結(jié)束后3個階段，共有8個核授權(quán)模型。

1）preA0：由授權(quán)決定的使用控制決策，決策判定發(fā)生在訪問之前，且在訪問之前、訪問過程中、訪問之后沒有屬性更新操作。

2）preA1：由授權(quán)決定的使用控制決策，決策判定發(fā)生在訪問之前，且在執(zhí)行訪問操作前完成主客體相關(guān)屬性的更新。

3）preA2：由授權(quán)決定的使用控制決策，決策判定發(fā)生在訪問之前，且在執(zhí)行訪問的過程中完成主客體相關(guān)屬性的更新。

4）preA3：由授權(quán)決定的使用控制決策，決策判定發(fā)生在訪問之前，且在訪問結(jié)束后完成主客體相關(guān)屬性的更新。

5）onA0：由授權(quán)決定的使用控制決策，決策判定發(fā)生在訪問過程中，且在訪問之前、訪問過程中、訪問之后沒有屬性更新操作。

6）onA1：由授權(quán)決定的使用控制決策，決策判定發(fā)生在訪問過程中，且在執(zhí)行訪問操作前完成主客體相關(guān)屬性的更新。

7）onA2：由授權(quán)決定的使用控制決策，決策判定發(fā)生在訪問過程中，且在執(zhí)行訪問的過程中完成主客體相關(guān)屬性的更新。

8）onA3：由授權(quán)決定的使用控制決策，決策判定發(fā)生在訪問過程中，且在訪問結(jié)束后完成主客體相關(guān)屬性的更新。

3.1.1核模型preA0

在preA0中授權(quán)決策由系統(tǒng)執(zhí)行，且發(fā)生在訪問之前，同時主體和客體的屬性在訪問全程中沒有任何變化。利用TCSP#描述的preA0如下。

preA0_S_O_R（s，o，r）=tryaccess.s.o.r->if（P1 &&…&&Pn）｛permitaccess.s.o.r->doaccess.s.o.r->end. s.o.r->Skip｝else｛denyaccess.s.o.r->Skip｝

在preA0_S_O_R（s，o，r）中，P1&&…&&Pn是建立在主體和客體屬性上的授權(quán)謂詞。當(dāng)該謂詞為真時，訪問得到許可，并開始執(zhí)行，否則訪問被系統(tǒng)予以拒絕。為了區(qū)分不同的訪問進(jìn)程，在進(jìn)程的命名上，preA0表示決策和屬性更新的類型，S表示具有某種共同特性的主體集，如STUDENT表示由學(xué)生形成的主體的集合，O表示具有某種共同特性的客體集，如 FILE表示由文件形成的集合，R表示權(quán)限的類型，如READ表示讀權(quán)限。為了方便讀者體會如何使用TCSP#建模以及與以往形式化規(guī)范工作的區(qū)別，本文的實(shí)例盡量選自文獻(xiàn)［5］。

實(shí)例 1在強(qiáng)制訪問控制模型中，每個主體和客體均有一個安全級別，主體對客體的訪問主要通過安全級別的比較來實(shí)現(xiàn)?，F(xiàn)在以經(jīng)典的面向信息保密的BLP（Bell-LaPadula）［17］模型為例，來說明如何利用 TCSP#具體描述 preA0策略。BLP對主體和客體都賦予一定的安全級別，同時將安全級別進(jìn)行排序。用戶不能改變自身和客體的安全級別，只有管理員才能夠確定用戶的訪問權(quán)限。在實(shí)施訪問控制時，系統(tǒng)先對訪問主體和受控客體的安全級別屬性進(jìn)行比較，再決定訪問主體能否訪問受控客體。應(yīng)用于保障信息保密性的訪問主要有以下2種方式。

1）向下讀：主體安全級別高于客體的安全級別時允許查閱的讀操作。

2）向上寫：主體安全級別低于客體的安全級別時允許寫操作。

第一種方式的 TCSP#規(guī)范描述如下，其中s_level，o_level分別表示主體和客體的安全等級。

preA0_S_O_READ（s，o，r）=tryaccess.s.o.r->if（s_level>o_level）｛permitaccess.s.o.r->doaccess.s.o.r -> end.s.o.r ->Skip｝else｛denyaccess.s.o.r ->Skip｝

第二種方式的TCSP#規(guī)范描述如下。

preA0_S_O_WRITE（s，o，w）=tryaccess.s.o.w-> if（s_level<=o_level）｛permitaccess.s.o.w->doaccess. s.o.w->end.s.o.w->Skip｝else｛denyaccess.s.o.w->Skip｝

3.1.2核模型preA1

preA1與preA0的主要不同在于在訪問控制實(shí)施之前主客體的屬性可能會被更新。一般情況下，更新操作發(fā)生在主體發(fā)出訪問請求且請求得到許可之后。利用TCSP#描述的preA1如下。

preA1_S_O_R（s，o，r）=tryaccess.s.o.r->if（P1&& …&&Pn）｛permitaccess.s.o.r->preupdate.s.o.r｛…｝-> doaccess.s.o.r->end.s.o.r->Skip｝else｛denyaccess.s.o.r -> Skip｝

在屬性更新操作preupdate｛…｝中可以完成多個屬性的更新，同時還有時序性約束，如preupdate｛x=x+1；y=y+1｝表示先完成對x的更新，然后完成對y的更新。

實(shí)例 2在一個按次計(jì)費(fèi)的數(shù)字版權(quán)保護(hù)系統(tǒng)中，主體擁有屬性credit，表示擁有的存款，客體擁有屬性value，表示每次訪問的代價。當(dāng)主體的credit超過客體的value時，主體可以對客體執(zhí)行讀的訪問。在訪問開始前，主體的存款 credit將減少value。具體的訪問過程如下。

preA1_S_O_READ（s，o，r）=tryaccess.s.o.r->if（s_credit>=o_value）｛permitaccess.s.o.r->preupdate. s.o.r｛s_credit=s_credit-o_value；｝->doaccess.s.o.r-> end.s.o.r->Skip｝else｛denyaccess.s.o.r->Skip｝

3.1.3核模型preA2

在模型preA2中，授權(quán)決策由系統(tǒng)在訪問之前檢測，且在訪問過程中會有多個屬性值被更新。利用TCSP#描述的preA2如下。

preA2_S_O_R（s，o，r）=tryaccesss.o.r->if（P1&&…&&Pn）｛permitaccess.s.o.r->doaccess.s.o.r->onup date.s.o.r｛…｝->end.s.o.r->Skip｝else｛denyaccess.s.o.r->Skip｝

3.1.4核模型preA3

在模型preA3中，授權(quán)決策由系統(tǒng)在訪問之前檢測，且在訪問結(jié)束后會有多個屬性值被更新。利用TCSP#描述的preA3如下。

preA3_S_O_R（s，o，r）=tryaccesss.o.r->if（P1&& …&&Pn）｛permitaccess.s.o.r->doaccess.s.o.r->end. s.o.r->postupdate.s.o.r｛…｝->Skip｝else｛denyacc ess.s.o.r->Skip｝

實(shí)例 3在一個基于會員的數(shù)字版權(quán)管理系統(tǒng)中，讀者擁有屬性expense和readingGroup，書擁有屬性readingGroup和readingCost。如果讀者和書屬于同一個閱讀組，則讀者可以閱讀此書，同時閱讀結(jié)束后讀者的閱讀費(fèi)用在原 expense的基礎(chǔ)上增加readingCost。具體訪問控制過程如下。

preA3_S_O_READ（s，o，r）=tryaccesss.o.r -> if（s_readingGroup==o_readingGroup）｛permitacc ess.s.o.r->doaccess.s.o.r->end.s.o.r->postupdate.s.o. r｛s_expense=s_expense+o_readingCost｝->Skip｝els e｛denyaccess.s.o.r->Skip｝

3.1.5核模型onA0

在授權(quán)決策由系統(tǒng)在訪問之前檢測的模式下，訪問請求得到許可后將不再進(jìn)行安全檢查。在模型onA0中，授權(quán)決策將被重復(fù)檢測，一旦檢測到授權(quán)謂詞真值為假，系統(tǒng)立即撤銷此次訪問。在訪問的過程中，主體隨時可能結(jié)束訪問，引入事件continue.s.o.r表示主體繼續(xù)訪問，引入事件nocontinue.s.o.r表示主體主動結(jié)束訪問。利用TCSP#描述的onA0如下。

onA0_S_O_R_1（s，o，r）=tryaccess.s.o.r->onA0_ S_O_R_2（s，o，r）

onA0_S_O_R_2（s，o，r）=doaccess.s.o.r->if（P1&&…&&Pn）｛continue.s.o.r->onA0_S_O_R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r->Skip｝else｛revokeaccess. s.o.r->Skip｝

實(shí)例 4在一個組織機(jī)構(gòu)中，用戶 Bob（角色為employee）可以參與該組織的一個短期項(xiàng)目。臨時證書temp_cert用以證明Bob的身份。當(dāng)Bob訪問項(xiàng)目中的敏感信息時，他的數(shù)字證書temp_cert會被重復(fù)檢測。如果檢測到證書在證書撤銷列表中，Bob的臨時身份將會被撤銷，進(jìn)而他不能繼續(xù)對敏感信息進(jìn)行訪問。訪問控制過程如下。

onA0_S_O_R_1（s，o，r）=tryaccess.s.o.r->onA0_ S_O_R_2（s，o，r）

onA0_S_O_R_2（s，o，r）=doaccess.s.o.r->if（s_rol e==employee&&s_temp_cert==1）｛continue.s.o.r-> onA0_S_O_R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r-> Skip｝else｛revokeaccess.s.o.r->Skip｝

上述控制過程中，s_temp_cert==1表示證書不在撤銷列表中。

3.1.6核模型onA1

與模型onA0不同之處主要在于，模型onA1中主客體的屬性在訪問開始前可以被更新。利用TCSP#描述的onA1如下。

onA1_S_O_R_1（s，o，r）=tryaccess.s.o.r->preupd ate.s.o.r｛…｝->onA1_S_O_R_2（s，o，r）

onA1_S_O_R_2（s，o，r）=doaccess.s.o.r->if（P1&&…&&Pn）｛continue.s.o.r->onA1_S_O_R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r->Skip｝else｛revokeaccess. s.o.r->Skip｝

3.1.7核模型onA2

與模型 onA1的不同之處主要在于，模型onA2中主客體的屬性在訪問過程中重復(fù)被更新。

利用TCSP#描述的onA2如下。

onA2_S_O_R_1（s，o，r）=tryaccess.s.o.r->onA2_ S_O_R_2（s，o，r）

onA2_S_O_R_2（s，o，r）=doaccess.s.o.r->onup date.s.o.r｛…｝-> if（P1&&…&&Pn）｛continue.s.o.r-> onA2_S_O_R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r-> Skip｝else｛revokeaccess.s.o.r->Skip｝

3.1.8核模型onA3

與模型onA2的不同之處主要在于模型onA3中主客體的屬性在訪問結(jié)束后進(jìn)行更新。利用TCSP#描述的onA3如下。

onA3_S_O_R_1（s，o，r）=tryaccess.s.o.r->onA3_ S_O_R_2（s，o，r）

onA3_S_O_R_2（s，o，r）=doaccess.s.o.r->if（P1&&…&&Pn）｛continue.s.o.r->onA3_S_O_R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r->postupdate.s.o.r｛…｝-> Skip｝else｛revokeaccess.s.o.r->postupdate.s.o.r｛…｝->Skip｝

實(shí)例 5考察一個數(shù)字版權(quán)管理系統(tǒng)，該系統(tǒng)允許對客體的并發(fā)訪問數(shù)量不超過10個。任何一個用戶在任何時候只能發(fā)送一個新的訪問請求。當(dāng)系統(tǒng)并發(fā)訪問的數(shù)量達(dá)到10時，新的訪問請求的到達(dá)必將導(dǎo)致一個在線進(jìn)行的訪問控制被撤銷。撤銷的策略有多種，可以依據(jù)訪問的開始時間、訪問過程中的空閑時間或者訪問持續(xù)的時間。對于不同的策略需要定義不同的系統(tǒng)屬性。設(shè)o表示客體，s表示主體，定義如下幾個屬性。

1）s_o_accessing表示主體s對客體o的訪問，值為1表示主體s發(fā)出了對客體o的訪問請求，值為0表示主體s沒有發(fā)出對客體o的訪問請求。

2）o_accessing_number表示訪問客體o的主體的數(shù)量。

3）sys_clock表示系統(tǒng)時間，為系統(tǒng)屬性。

4）s_o_starttime是主體屬性，表示主體s開始對客體o開始訪問的時間。

5）minstarttime表示最先開始訪問的時間。

現(xiàn)在以最早開始時間為撤銷策略為例。因?yàn)閷傩缘母掳l(fā)生在訪問開始前和訪問結(jié)束后，所以，整體的使用控制策略定義為 onA1與onA3的組合。

onA13_S_O_R_1（s，o，r）=tryaccess.s.o.r->preup date.s.o.r ｛s_o_accessing=1； o_accessing_number=o_accessing_number+1；s_o_starttime=sys_clock｝-> onA13_S_O_R_2（s，o，r）

onA13_S_O_R_2（s，o，r）=doaccess.s.o.r->if（！（o_ accessing_number==11&&o_s_starttime==minstarttime））｛continute.s.o.r->onA13_S_O_R_2（s，o，r）［］nocontinute.s.o.r->end.s.o.r->postupdate.s.o.r｛o_ accessing_number=o_accessing_number-1； s_o_ starttime=0｝->Skip｝else｛revokeaccess.s.o.r-> postupdate.s.o.r｛s_o_accessing_s=0；o_accessing_s_ number=o_accessing_s_number-1；s_o_starttime=0｝->Skip｝

3.2義務(wù)核模型的規(guī)約

義務(wù)是 UCON中除了授權(quán)之外另外一個重要的構(gòu)件。本節(jié)將探討義務(wù)的TCSP#規(guī)范。由于訪問決策的連續(xù)性，在UCON中有2種類型的義務(wù)：預(yù)義務(wù)，即在主體開始訪問客體前必須完成的事件；在線義務(wù)，即在訪問的過程中必須完成的事件。類似于授權(quán)核模型，基于更新操作發(fā)生的時間段，可以進(jìn)一步將義務(wù)核模型分解成8個子模型。

1）preB0：由義務(wù)決定的使用控制決策，決策判定發(fā)生在訪問之前，且在訪問之前、訪問過程中、訪問之后沒有屬性更新操作。

2）preB1：由義務(wù)決定的使用控制決策，決策判定發(fā)生在訪問之前，且在執(zhí)行訪問操作前完成主客體相關(guān)屬性的更新。

3）preB2：由義務(wù)決定的使用控制決策，決策判定發(fā)生在訪問之前，且在執(zhí)行訪問的過程中完成主客體相關(guān)屬性的更新。

4）preB3：由義務(wù)決定的使用控制決策，決策判定發(fā)生在訪問之前，且在訪問結(jié)束后完成主客體相關(guān)屬性的更新。

5）onB0：由義務(wù)決定的使用控制決策，決策判定發(fā)生在訪問過程之中，且在訪問之前、訪問過程中、訪問之后沒有屬性更新操作。

6）onB1：由義務(wù)決定的使用控制決策，決策判定發(fā)生在訪問過程之中，且在執(zhí)行訪問操作前完成主客體相關(guān)屬性的更新。

7）onB2：由義務(wù)決定的使用控制決策，決策判定發(fā)生在訪問過程之中，且在執(zhí)行訪問的過程中完成主客體相關(guān)屬性的更新。

8）onB3：由義務(wù)決定的使用控制決策，決策判定發(fā)生在訪問過程之中，且在訪問之后主客體的屬性將會被更新。

3.2.1核模型preB0

preB0規(guī)定只有當(dāng)所有的義務(wù)事件完成后，訪問才能被許可。以一個義務(wù)事件ob為例來說明preB0對應(yīng)的訪問控制流程，主體可以執(zhí)行義務(wù)，也可以不執(zhí)行，引入事件noob表示主體沒有執(zhí)行義務(wù)ob。利用TCSP#描述的preB0如下。

preB0_S_O_R（s，o，r）=tryaccess.s.o.r->（ob.s.o.r-> doaccess.s.o.r->end.s.o.r->Skip［］noob.s.o.r-> denyaccess.s.o.r ->Skip）

實(shí)例 6在一個在線電子市場中，客戶為了完成訂購，需要點(diǎn)擊接受訂購協(xié)議的同意按鈕。定義事件click_agreement表示客戶點(diǎn)擊了接受訂購協(xié)議的同意按鈕。該策略的TCSP#規(guī)范如下。

preB0_S_O_R（s，o，r）=tryaccess.s.o.r->（click_ agreement.s.o.r->doaccess.s.o.r->end.s.o.r->Skip［］nonclick_agreement.s.o.r -> denyaccess.s.o.r ->Skip）

3.2.2核模型preB1

PreB1規(guī)定只有當(dāng)所有的義務(wù)事件完成后，訪問才能被許可，且在訪問開始之前需要更新主客體的屬性。利用TCSP#描述的preB1如下。

preB1_S_O_R（s，o，r）=tryaccess.s.o.r->（ob. s.o. r->preupdate.s.o.r｛…｝->doaccess.s.o.r->end.s.o.r［］noob.s.o.r->denyaccess.s.o.r->Skip）

3.2.3核模型preB2

PreB2規(guī)定只有當(dāng)所有的義務(wù)事件完成后，訪問才能被許可，且在訪問過程中更新主客體的屬性。利用TCSP#描述的preB2如下。

preB2_S_O_R（s，o，r）=tryaccess.s.o.r->（ob.s.o.r->doaccess.s.o.r->onupdate.s.o.r｛…｝->end.s.o.r-> Skip［］nonob.s.o.r->denyaccess.s.o.r->Skip）

3.2.4核模型PreB3

PreB3規(guī)定只有當(dāng)所有的義務(wù)事件完成后，訪問才能被許可，且在訪問結(jié)束后更新主客體的屬性。利用TCSP#描述的preB3如下。

preB3_S_O_R（s，o，r）=tryaccess.s.o.r->（ob.s.o.r ->doaccess.s.o.r->end.s.o.r->postupdate.s.o.r｛…｝-> Skip［］nonob.s.o.r->denyaccess.s.o.r ->Skip）

實(shí)例7在實(shí)例7中，當(dāng)顧客完成訂購，在訂單列表中添加一項(xiàng)訂單時，訂單列表需要更新。引入主體屬性s_o_order表示主體s是否對客體o下了訂單：值為1表示下了訂單，值為0表示沒有下訂單。此策略的TCSP#規(guī)范表示如下。

preB3_S_O_R（s，o，r）=tryaccess.s.o.r->（ob.s.o.r->doaccess.s.o.r->end.s.o.r->postupdate.s.o.r｛s_o_ order=1｝->Skip［］nonob.s.o.r->denyaccess.s.o.r->Skip）

3.2.5核模型onB0

onB0規(guī)定主體必須在訪問控制的過程中重復(fù)執(zhí)行義務(wù)事件，否則訪問將被取消，且在整個訪問過程中無需更新主客體的屬性。利用TCSP#描述的onB0如下。

onB0_S_O_R_1（s，o，r）=tryaccess.s.o.r->onB0_ S_O_R_2（s，o，r）

onB0_S_O_R_2（s，o，r）=doaccess.s.o.r->（ob.s.o. r->（continute.s.o.r->onB0_S_O_R_2（s，o，r）［］nocont inue.s.o.r->end.s.o.r->Skip）［］noob.s.o.r->revo keaccess.s.o.r->Skip）

實(shí)例 8為了使用在線服務(wù)，廣告標(biāo)語必須在客戶端打開，否則服務(wù)就失效。該控制策略的TCSP#規(guī)范表示如下。

onB0_S_O_R_1（s，o，r）=tryaccess.s.o.r->onB0_ S_O_R_1（s，o，r）

onB0_S_O_R_2（s，o，r）=doaccess.s.o.r->（openban ner.s.o.r->（continute.s.o.r->onB0_S_O_R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r->Skip）［］noopenbanner.s. o.r->revokeaccess.s.o.r->Skip）

3.2.6核模型onB1

onB1規(guī)定主體必須在訪問控制的過程中重復(fù)執(zhí)行義務(wù)事件，否則訪問將被取消，且在訪問開始前更新主客體的屬性。利用 TCSP#描述的onB1如下。

onB1_S_O_R_1（s，o，r）=tryaccess.s.o.r->preupd ate.s.o.r｛…｝-> onB2_S_O_R_1（s，o，r）

onB1_S_O_R_2（s，o，r）=doaccess.s.o.r->（ob.s.o. r->（continute.s.o.r->onB1_S_O_R_2（s，o，r）［］noconti nue.s.o.r->end.s.o.r->Skip）［］noob.s.o.r->revokeacce ss.s.o.r ->Skip）

3.2.7核模型onB2

onB2規(guī)定主體必須在訪問控制的過程中重復(fù)執(zhí)行義務(wù)事件，否則訪問將被取消，且在訪問過程中重復(fù)更新主客體的屬性。利用TCSP#描述的onB2如下。

onB2_S_O_R_1（s，o，r）=tryaccess.s.o.r->onB2_ S_O_R_2（s，o，r）

onB2_S_O_R_2（s，o，r）=doaccess.s.o.r->oneupdate. s.o.r｛…｝->（ob.s.o.r->（continute.s.o.r->onB2_S_O_ R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r->Skip）［］noob. s.o.r->revokeaccess.s.o.r->Skip）

3.2.8核模型onB3

onB3規(guī)定主體必須在訪問控制的過程中重復(fù)執(zhí)行義務(wù)事件，否則訪問將被取消，且在訪問結(jié)束或者撤銷后更新主客體的屬性。利用TCSP#描述的onB3如下。

onB2_S_O_R_1（s，o，r）=tryaccess.s.o.r-> onB2_ S_O_R_2（s，o，r）

onB2_S_O_R_2（s，o，r）=doaccess.s.o.r->（ob.s.o. r->（continute.s.o.r->onB2_S_O_R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r->postupdate.s.o.r｛…｝->Skip）［］noob.s.o.r->revokeaccess.s.o.r->postupdate.s.o.r｛…｝-> Skip）

實(shí)例 9在一個在線服務(wù)應(yīng)用中，用戶需要每隔30 min點(diǎn)擊廣告窗口，否則服務(wù)自動撤銷。主體屬性 s_usagetime表示服務(wù)應(yīng)用的在線使用時間，訪問開始時s_usagetime的初始值設(shè)置為0時，在訪問過程中s_usagetime不斷增加，在訪問結(jié)束后s_usagetime又被設(shè)置為0，因此該訪問控制策略由onB1、onB2、onB3三者組合而成。

此實(shí)例中義務(wù)的執(zhí)行是有條件的，即只有當(dāng)在線時間達(dá)到30 min時才必須執(zhí)行點(diǎn)擊廣告的事件，因此在重復(fù)檢測的過程中需要加入條件進(jìn)行判斷。以下是該控制流程的TCSP#規(guī)范。

onB123_S_O_R_1（s，o，r）=tryaccess.s.o.r->preu pdate｛s_usagetime=0｝->onB123_S_O_R_2（s，o，r）

onB123_S_O_R_2（s，o，r）=doaccess.s.o.r->onup date1.s.o.r｛s_usagetime=s_usagetime+1｝->if（s_usag etime==30）｛（clickad.s.o.r->onupdate2.s.o.r ｛s_ usagetime=0｝->（continute.s.o.r->onB123_S_O_R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r->postupdate.s.o.r ｛s_usagetime=0｝->Skip））［］（noclickad.s.o.r-> revokeaccess.s.o.r->postupdate.s.o.r｛s_usagetime=0｝->Skip）｝else｛（continute.s.o.r->onB123_S_O_R_2（s，o，r））［］（nocontinue.s.o.r->end.s.o.r->postupdate.s.o. r｛s_usagetime=0｝-> Skip）｝

3.3條件核模型的規(guī)約

條件構(gòu)件是面向環(huán)境和系統(tǒng)的決策因素，條件謂詞用于估算當(dāng)前的環(huán)境和系統(tǒng)狀態(tài)。與授權(quán)、義務(wù)不同，條件不能改變主客體的屬性。基于條件謂詞估算的時間點(diǎn)的不同，條件核模型可以分為預(yù)條件和在線條件2種類型。

3.3.1核模型preC0

在模型preC0中條件謂詞必須在訪問開始前檢測，且沒有任何的主客體屬性被更新。利用TCSP#描述的preC0如下。

preC0_S_O_R（s，o，r）=tryaccess.s.o.r->if（PC1 &&… &&PCn）｛permitaccess.s.o.r->doaccess.s.o.r-> end.s.o.r->Skip｝else ｛denyaccess.s.o.r ->Skip｝

3.3.2核模型onC0

在模型 onC0中條件謂詞在訪問的過程中不斷被檢測，如果謂詞真值為真，則繼續(xù)訪問，否則立即撤銷當(dāng)前的訪問。此外在訪問整個過程中沒有任何的主客體屬性被更新。利用TCSP#描述的onC0如下。

onC0_S_O_R_1（s，o，r）=tryaccess.s.o.r->onC0_ S_O_R_2（s，o，r）

onC0_S_O_R_2（s，o，r）=doaccess.s.o.r->if（PC 1&&…&&PCn）｛continue.s.o.r->onC0_S_O_R_2（s，o，r）［］nocontinue.s.o.r->end.s.o.r->Skip｝else｛revokeaccess. s.o.r->Skip｝

實(shí)例 10訪問控制策略定義一個值日班的職員（角色為dayshifter）僅僅在白天能夠訪問對象、定義currenttime為系統(tǒng)屬性，表示當(dāng)前時間。該策略是 preA0、preC0、onC0的組合，TCSP#描述如下

preA0_preC0_OnC0_S_O_R_1（s，o，r）=tryacces s.s.o.r->if（s_role==dayshifter&&8am<=currenttime <=5pm）｛permitdoaccess.s.o.r->doaccess.s.o.r-> preA0_preC0_OnC0_S_O_R_2（s，o，r）｝else｛denya ccess.s.o.r ->Skip｝

preA0_preC0_OnC0_S_O_R_2（s，o，r）=if（8am<=currenttime<=5pm）｛doaccess.s.o.r->（continue.s.o.r ->preA0_preC0_OnC0_S_O_R_2（s，o，r）［］nocontinute. s.o.r->end.s.o.r->Skip）｝else｛revokeaccess.s.o.r-> Skip｝

4　并發(fā)、時間約束、非確定性

UCON應(yīng)用于計(jì)算無處不在的環(huán)境，因此訪問的并發(fā)性、訪問時間的控制與訪問的非確定性是UCON中最重要的特性。目前還沒有任何工作對此 3個問題進(jìn)行詳細(xì)探討，文獻(xiàn)［10］也將此問題列為UCON的主要挑戰(zhàn)。如何建立正確描繪此3個問題的模型至關(guān)重要，本節(jié)將從建模的角度對此3個問題展開詳細(xì)分析。

4.1并發(fā)

UCON的服務(wù)對象是分布式、網(wǎng)絡(luò)化系統(tǒng)，在某一段時間同一個主體訪問不同客體，不同主體訪問同一個主體將是常態(tài)，因此并發(fā)訪問是UCON應(yīng)用中一個非?；A(chǔ)的特征。在訪問過程中屬性的更新操作將會影響另外一個正在發(fā)生的訪問控制的授權(quán)決策。由于主體的行為不受約束，它可以在任意時刻發(fā)起對任意客體的訪問，依據(jù)并發(fā)的復(fù)雜性，將并發(fā)分成多種情況，以建立不同并發(fā)類型的TCSP#規(guī)范。以實(shí)例12為例，進(jìn)行詳細(xì)闡述。

實(shí)例 11在一個基于用戶預(yù)消費(fèi)的數(shù)字版權(quán)管理系統(tǒng)中，讀者s擁有屬性expense，表示賬戶里的預(yù)存款，書o擁有屬性readingcost表示用戶閱讀本書一次的價格。訪問控制策略是用戶發(fā)出請求后，如果賬戶的存款余額不小于閱讀的代價，則此次訪問請求得到許可，并從預(yù)存款中扣除相應(yīng)的價格。此外假設(shè)管理系統(tǒng)已經(jīng)規(guī)定同一本書被多個用戶閱讀的次數(shù)累計(jì)不超過K次。

現(xiàn)在假設(shè)有兩個讀者s0和s1，其初始擁有的expense分別為11和9。假設(shè)有兩本書b0與b1。b0的屬性readingcost為5，b1的屬性readingcost 為4。定義數(shù)組s［2］，s［i］（i=0，1）表示第i個主體的屬性expense。定義數(shù)組b［2］，b［i］（i=0，1）表示第i個客體的屬性readingcost。定義數(shù)組number［2］，number［i］（i=0，1）用以記錄客體i被閱讀的次數(shù)，初始值為0。

1）Type-1 并發(fā)：某個時刻主體可以發(fā)出對客體的單次訪問。

在訪問控制流程中主客體的屬性將在訪問開始前予以更新，因此屬于核模型 preA1，具體的TCSP#規(guī)范如下。

preA1_S_O_R_Type_1（i，j，r）=tryaccess.i.j.r->if（s［i］>=b［j］&&number［j］

｛permitaccess.s.o.r->preupdate.i.j.r｛s［i］=s［i］-b［j］；number［j］=number［j］+1；｝->doaccess.i.j.r->end.i.j.r ->Skip｝else｛denyaccess.i.j.r->Skip｝

2）Type-2并發(fā)：上次訪問結(jié)束后主體可以繼續(xù)對同一客體發(fā)出多次相同的訪問請求。

在訪問過程中主客體的屬性將在訪問開始前予以更新，因此屬于核模型 preA1。同時允許訪問結(jié)束后主體可以對客體繼續(xù)訪問，這種許可在TCSP#中可以使用進(jìn)程P（）=a->P（）來定義，具體的TCSP#規(guī)范如下。

preA1_S_O_R_Type_2（i，j，r）=tryaccess.i.j.r->if（s［i］>=b［j］&&number［j］ preupdate.i.j.r｛s［i］=s［i］-b［j］；number［j］=number［j］+1；｝->doaccess.i.j.r->end.i.j.r->preA1_S_O_R_Typ e_2（i，j，r）｝else｛denyaccess.i.j.r->preA1_S_O_R_Typ e_2（i，j，r）｝

Type-2 并發(fā)與Type-1并發(fā)的主要區(qū)別在于，將preA1_S_O_R_Type_1（i，j，r）中所有Skip事件替換為preA1_S_O_R_Type_2（i，j，r）。依據(jù)TCSP#的語義解釋，當(dāng)事件end或者denyaccess執(zhí)行結(jié)束后，按照 preA1_S_O_R_Type_2（i，j，r）的規(guī)范重新開始運(yùn)行，從而實(shí)現(xiàn)了新一輪次的訪問。

3）Type-3并發(fā)：在一段時間內(nèi)主體可以發(fā)出對同一客體的多次相同的訪問請求，且并不需要等待上次訪問的結(jié)束，即所設(shè)計(jì)的進(jìn)程必須能夠描述在訪問過程中主體可以隨時發(fā)出對客體的又一次訪問請求的規(guī)范。

在 TCSP#中算子<>實(shí)現(xiàn)了多個進(jìn)程之間的隨機(jī)選擇，因此在原理上可以對進(jìn)程preA1_S_O_ R_Type_2（i，j，r）中的每一個事件添加一個可以發(fā)出訪問請求的選項(xiàng)來達(dá)到一段時間內(nèi)發(fā)出多次訪問請求的目的。但是，<>實(shí)現(xiàn)的是進(jìn)程之間而不是事件之間的隨機(jī)選擇，因此首先要將 preA1_ S_O_R_Type_2（i，j，r）中的每一個事件重新定義為一個進(jìn)程，然后按照preA1_S_O_ R_Type_2（i，j，r）組織進(jìn)程之間的序，具體的TCSP#規(guī)范如下。

Proc_tryaccess（i，j，r）=tryaccess.i.j.r->if（s［i］>=b ［j］&&number［j］

Proc_permitaccess（i，j，r）=permitaccess.i.j.r->Pr oc_preupdate（i，j，r）<> preA1_S_O_R_Type_3（i，j，r）。

Proc_preupdate（i，j，r）=preupdate.i.j.r｛s［i］=s［i］-b［j］； number［j］=number［j］+1；｝->Proc_doaccess（i，j，r）<> preA1_S_O_R_Type_3（i，j，r）

Proc_doaccess（i，j，r）=doaccess.i.j.r->Proc_end（i，j，r）<> preA1_S_O_R_Type_3（i，j，r）

Proc_denyaccess（i，j，r）=denyaccess.i.j.r->preA1_ S_O_R_Type_3（i，j，r）

Proc_end（i，j，r）=end.i.j.r->preA1_S_O_R_Type _3（i，j，r）

preA1_S_O_R_Type_3（i，j，r）=Proc_tryaccess（i，j，r）<> preA1_S_O_R_Type_3（i，j，r）

4）Type-4并發(fā)：同一時間主體可以對客體發(fā)出多次相同的訪問。

定義進(jìn)程 preA1_S_O_R_Type_4（i，j，r，k）來描繪某個時刻主體可以發(fā)出對客體的單次訪問。與preA1_S_O_R_Type_1（i，j，r）的不同之處在于引入k用來標(biāo)記發(fā)出的第幾次訪問請求。

preA1_S_O_R_Type_4（i，j，r，k）=tryaccess.i.j.r-> if（s［i］>=b［j］&&number［j］doaccess.i.j.r. k->end.i.j.r->Skip｝ else ｛denyaccess. i.j.r.k-> Skip｝

定義進(jìn)程preA1_S_O_R_Type_4_parallel（i，j，r，m）=preA1_S_O_R_Type_4（i，j，r，0）||…||preA1_S_ O_R_Type_4（i，j，r，m-1）。

進(jìn)程preA1_S_O_R_Type_4_parallel中，符號||表示多個進(jìn)程之間的平行組合。為了實(shí)現(xiàn)同時發(fā)出多次訪問請求的描述，引入了事件tryaccess.i.j.r進(jìn)行同步。平行組合意味著preA1_S_O_R_Type_4（i，j，r，0），…，preA1_S_O_R_Type_4（i，j，r，m-1）必須同時執(zhí)行tryaccess.i.j.r事件，從而實(shí)現(xiàn)了m個進(jìn)程同時發(fā)出訪問請求的目的。

5）Type-5并發(fā)：在一段時間內(nèi)主體可以對不同的客體產(chǎn)生訪問請求。

在TCSP#中多進(jìn)程之間的交互意味著在任意時刻可從多進(jìn)程中任意選擇一個進(jìn)程執(zhí)行，利用交互算子|||定義進(jìn)程 preA1_S_O_R_Type_5（i，r）=preA1_S_O_R_Type_1（i，0，r）|||… |||preA1_S_O_R_ Type_1（i，n-1，r）。算子|||確保了在任意時刻可從 n個子進(jìn)程中選擇一個進(jìn)程執(zhí)行，從而達(dá)到主體對不同客體的訪問。

6）Type-6并發(fā)：在一段時間內(nèi)不同主體可以對相同的客體產(chǎn)生訪問請求。

與Type-5并發(fā)類似，定義進(jìn)程preA1_S_O_ R_Type_6（j，r）=preA1_S_O_R_Type_1（0，j，r）|||… ||| preA1_S_O_R_Type_6（m-1，j，r）。

7）Type-7并發(fā)：同一時間主體可以對不同的客體產(chǎn)生訪問請求。

首先定義進(jìn)程 preA1_S_O_R_Type_7（i，j，r）描繪主體對客體的單次訪問，與 preA1_S_O_R_ Type_1（i，j，r）不同的是，這里引入事件tryaccess用于進(jìn)程之間的同步

preA1_S_O_R_Type_7（i，j，r）=tryaccess->if（s［i］>=o［j］&&number［j］doaccess.i.j.r->end.i.j.r ->Skip｝else ｛denyaccess.i.j.r->Skip｝

定義進(jìn)程preA1_S_O_R_Type_7_syn=preA1_ S_O_R_Type_7（i，0，r）||…||preA1_S_O_R_Type_7（i，n-1，r）。在preA1_S_O_R_Type_7_syn中，preA1_ S_O_R_Type_7（i，j，r）（j=0，…，n-1）必須同時執(zhí)行事件 tryaccess，然后獨(dú)立運(yùn)行，從而實(shí)現(xiàn)了同一時間點(diǎn)主體對不同客體產(chǎn)生訪問的請求。

8）Type-8并發(fā)：同一時間不同主體可以對相同的客體產(chǎn)生訪問請求。

與Type-7并發(fā)類似，定義進(jìn)程preA1_S_O_ R_Type_8_syn=preA1_S_O_R_Type_7（0，0，r）||…|| preA1_S_O_R_Type_7（m-1，0，r）。

9）Type-9并發(fā)：在一段時間內(nèi)不同主體可以對不同的客體產(chǎn)生訪問請求。

preA1_S_O_R_Type_9（）=preA1_r_Type_1（0，0 ，r）|||… |||preA1_r_Type_1（0，n-1，r）|||… ||| preA1_ r_Type_1（m-1，j，r）。|||表示進(jìn)程之間的交互執(zhí)行，因此上述進(jìn)程表示m個主體在一段時間內(nèi)對n個客體產(chǎn)生了訪問請求。

10）Type-10并發(fā)：同一時間不同主體可以對不同的客體產(chǎn)生訪問請求。

preA1_S_O_R_Type_10（）=preA1_S_O_R_Ty pe_7（0，0，r）||… ||preA1_S_O_R_Type_7（0，m-1，r）|||…||| preA1_S_O_R_Type_7（n-1，m-1，r）。在上述進(jìn)程中所有進(jìn)程必須同時執(zhí)行事件 tryaccess，從而實(shí)現(xiàn)同一時間不同主體可以對不同客體產(chǎn)生訪問請求。

11）Type-11并發(fā)：在一段時間內(nèi)不同主體可以對不同的客體產(chǎn)生多次訪問請求。

定義進(jìn)程 preA1_S_O_R_Type_11（）=preA1_ S_O_R_Type_2（0，0，r）|||…|||preA1_S_O_R_Type_2（0，n-1）|||…||| preA1_S_O_R_Type_2（m-1，n-1），其中 preA1_S_O_R_Type_2（i，j，r）實(shí)現(xiàn)了對同一客體的多次訪問請求，|||實(shí)現(xiàn)了訪問之間的交互。

12）Type-12并發(fā)：與系統(tǒng)環(huán)境的交互。

在實(shí)例11中，系統(tǒng)可能隨時往主體的賬戶上面充值，從而導(dǎo)致主體的expense隨時發(fā)生變化。對于此種情況，引入進(jìn)程 Proc_update（i）=update.i｛s［i］=s［i］+Fee｝->Skip描述充值過程，然后可通過算子|||與上述不同并發(fā)進(jìn)程實(shí)現(xiàn)交互。

TCSP#作為CSP的擴(kuò)展，在并發(fā)的描述上比CSP具有更強(qiáng)的表達(dá)能力，上述12種并發(fā)類型的成功描繪充分說明了TCSP#能夠完美刻畫UCON中的并發(fā)情況。

4.2時間控制

在UCON中當(dāng)主體發(fā)出訪問請求后，系統(tǒng)必須在一段時間內(nèi)進(jìn)行響應(yīng)，客體也必須在一定的時間內(nèi)完成義務(wù)事件的執(zhí)行。例如，在一個在線電子商務(wù)中，顧客必須點(diǎn)擊同意購買協(xié)議的按鈕才能繼續(xù)購物。這種點(diǎn)擊必須有時間限制，不可能為消費(fèi)者等待無窮時間，如可以設(shè)置如果在 5 min內(nèi)不點(diǎn)擊就撤銷此次訪問請求。為此考察以下幾種時間約束的TCSP#規(guī)范。

1）Type-1時間控制：請求發(fā)出后，必須在某段時間內(nèi)得到響應(yīng)，否則繼續(xù)發(fā)送訪問請求。

以核模型 preA0為例來說明時間控制的處理。定義如下進(jìn)程。

preA0_S_O_R_Type_1_Timing（s，o，r）=tryacce ss.s.o.r->（（if（P1&&…&&Pn）｛permitaccess.s.o.r-> doaccess.s.o.r->end.s.o.r->Skip｝else｛denyaccess.s. o.r->Skip｝）timeout［d］（denyaccess.s.o.r->preA0_S_ O_ R_Type_1_Timing（s，o，r）））

在preA0_S_O_R_ Type_1_Timing（s，o，r）中，timeout［d］表示主體執(zhí)行完事件tryaccess.s.o.r后，如果進(jìn)程 if（P1&&…&&Pn）｛permitaccess.s.o.r-> doaccess.s.o.r->end.s.o.r->Skip｝else｛denyaccess.s. o.r->Skip ｝在d個時間單元內(nèi)執(zhí)行了某個事件，則繼續(xù)按照此進(jìn)程的規(guī)范執(zhí)行，否則執(zhí)行進(jìn)程denyaccess.s.o.r->preA0_S_O_R_Type-1_Timing（s，o，r）。

2）Type-2時間控制：訪問得到許可后，必須在某段時間內(nèi)執(zhí)行完畢，否則撤銷此次訪問。

以核模型 preA0為例來說明時間控制的處理。定義如下進(jìn)程。

preA0_S_O_R_Type_2_Timing（s，o，r）=tryaccess.s.o.r->if（P1&&…&&Pn）｛permitaccess.s.o.r->（（doaccess.s.o.r->end.s.o.r->Skip）timeout［d］（denyaccess.s.o.r->preA0_S_O_R_Type_2_Timing（s，o，r）））｝else｛denyaccess.s.o.r->Skip ｝

在preA0_S_O_R_Type_2_Timing（s，o，r）中timeout［d］表示系統(tǒng)執(zhí)行完事件 permitaccess.s.o.r后，如果進(jìn)程doaccess.s.o.r->end.s.o.r->Skip在d個時間單元內(nèi)執(zhí)行了事件 doaccess.s.o.r，則繼續(xù)按照此進(jìn)程的規(guī)范執(zhí)行，否則執(zhí)行進(jìn)程denyaccess.s.o.r -> preA0_S_O_R_ Type_2_Timing（s，o，r）。

3）Type-3時間控制：義務(wù)的執(zhí)行必須在某個時間段內(nèi)完成，否則撤銷此次訪問。

以核模型 preB0為例來說明時間控制的處理。定義如下進(jìn)程。

preB0_S_O_R_Type_2_Timing（s，o，r）=tryaccess. s.o.r->（（ob.s.o.r->doaccess.s.o.r->end.s.o.r）timeout［d］（denyaccess.s.o.r->Skip））

在 preB0_S_O_R_Type_2_Timing中，進(jìn)程ob.s.o.r->doaccess.s.o.r->end.s.o.r的第一個事件ob.s.o.r必須在時間 d內(nèi)執(zhí)行，否則執(zhí)行進(jìn)程denyaccess.s.o.r->Skip。

實(shí)例12考察網(wǎng)格系統(tǒng)（grid system）中安全套接字（securing socket）的使用控制策略。主要有以下幾個訪問控制策略。

策略1套接字必須在發(fā)送數(shù)據(jù)前打開。

策略2只有注冊的用戶才可以打開編號在1 000到2 000之間的安全套接字進(jìn)行連接。

策略3每個用戶發(fā)送數(shù)據(jù)包的時間不能超過10 min。

策略1到策略3都沒有改變主客體的屬性，而且訪問控制決策是在訪問開始前進(jìn)行的，因此對應(yīng)的核模型為 preA0，同時訪問得到許可后，必須在10 min內(nèi)執(zhí)行完畢，對應(yīng)的時間控制類型為Type-2 Timing，具體進(jìn)程定義如下。

preA0_S_O_R_Type_2_Timing（s，o，r）=tryaccess. s.o.r->if（1000<=o<=2000）｛register.s.o.r->（（doaccess. s.o.r->end.s.o.r->Skip）timeout［10］（revokeaccess.s.o. r ）｝else｛denyaccess.s.o.r->Skip ｝

上述3種時間控制類型是UCON中的典型情況，應(yīng)用TCSP#成功刻畫了這些場景，充分說明了TCSP#刻畫時間控制的能力。

4.3非確定性

當(dāng)主體對客體的訪問請求得到許可后，主體通過執(zhí)行一系列的原語操作實(shí)現(xiàn)對客體的訪問。這些原語操作的執(zhí)行順序是隨機(jī)的，如用戶登錄到郵箱帳戶后可能采取的操作，但是不同的操作序列對主體和客體屬性的影響是不同的，從而導(dǎo)致后面的訪問控制受到影響。

在第5.1節(jié)的并發(fā)建模中利用一個抽象的事件doaccess來表示訪問執(zhí)行過程。假設(shè)doaccess可以分解成act_1，act_2，…，act_n等n個原子事件，這些事件的執(zhí)行順序是隨機(jī)的。通過交互算子|||實(shí)現(xiàn)訪問操作的隨機(jī)性，具體進(jìn)程定義為：（act_1->Skip|||…||| act_1->Skip）。

非確定性的另外一種呈現(xiàn)方式是訪問結(jié)束后屬性的更新。依據(jù)是正常結(jié)束還是撤銷結(jié)束的形式不同，屬性的更新操作也可能不同。如主體的信譽(yù)，正常結(jié)束可以提高主體的信譽(yù)，撤銷結(jié)束將降低主體的信譽(yù)。對于這種由于結(jié)束方式不同所引起的屬性更新的不確定性，分別用進(jìn)程end.i.j.r->postupdate.i.j.r和進(jìn)程 revokeaccess.i.j.r-> postupdate.i.j.r實(shí)現(xiàn)兩者之間的區(qū)別。

5　安全性分析

安全性分析是訪問控制系統(tǒng)中最基礎(chǔ)最重要的問題，其主要目標(biāo)是是判斷主體能否最終獲得對客體的訪問權(quán)限。對于傳統(tǒng)訪問控制模型，主要通過遍歷控制系統(tǒng)的可達(dá)狀態(tài)空間進(jìn)行安全性分析。這種方法也適用于UCON。

5.1全局可達(dá)空間的構(gòu)造

文獻(xiàn)［11］已經(jīng)證明如果主客體屬性的值域是有限的，且沒有新的主客體的產(chǎn)生，則 UCONA（僅僅包含授權(quán)因素的UCON模型）安全性問題是可判定的。這個問題比較容易理解，因?yàn)檫@ 2種約束保證了狀態(tài)空間的有窮性，可以通過窮舉狀態(tài)空間的方法來實(shí)現(xiàn)安全性分析。關(guān)于狀態(tài)空間的構(gòu)造，文獻(xiàn)［11］只給出了一個抽象的概念，即從初始狀態(tài)出發(fā)，通過執(zhí)行各種訪問控制請求計(jì)算下一步狀態(tài)，循環(huán)執(zhí)行從而計(jì)算出所有的可達(dá)空間?，F(xiàn)在的問題是如何構(gòu)造一個進(jìn)程，使在PAT中該進(jìn)程的可達(dá)空間就是整個UCON的可達(dá)空間。與文獻(xiàn)［11］一樣，主要考慮UCONA模型上的可達(dá)性分析。

構(gòu)造進(jìn)程代數(shù)的關(guān)鍵在于必須能夠表達(dá)任意時刻任意主體對任意客體發(fā)送任意的訪問請求。在給出構(gòu)造方法之前，先做一些假設(shè)：主體數(shù)目為m，客體數(shù)目為n，訪問權(quán)限只有r一種。具體的進(jìn)程構(gòu)造過程如下。

Procedure 1面向可達(dá)空間計(jì)算的進(jìn)程代數(shù)的構(gòu)造。

Step1構(gòu)造初始化進(jìn)程定義進(jìn)程 P（）= initialization｛…｝->Skip用于對變量進(jìn)行初始化。

Step2依據(jù) Type-1并發(fā)構(gòu)造某個時刻主體對客體的單次訪問流程，記為Proc_1（i，j，r）。

Step3依據(jù)Type-2 并發(fā)，在Proc_1（i，j，r）的基礎(chǔ)上構(gòu)造上次訪問結(jié)束后主體可以繼續(xù)對同一客體發(fā)出訪問請求的流程，記為Proc_2（i，j，r）。

Step4依據(jù) Type-3并發(fā)，在 Proc_2（i，j，r）的基礎(chǔ)上構(gòu)造在訪問過程中主體可以隨時發(fā)出對客體的再一次相同的訪問請求，記為 Proc_3（i，j，r）。

Step5構(gòu)造同一主體對 n個客體的交互訪問。定義進(jìn)程 Proc_4（i）=Proc_3（i，0，r）|||…|||Proc_3（i，n-1，r）。

Step6構(gòu)造任一主體對任一客體的交互訪問。定義進(jìn)程Proc_5（）=Proc_4（0）|||…|||Proc_4（m-1）。

Step7定義進(jìn)程Proc（）=P（）；Proc_5（）。

定理1Procedure 1構(gòu)造出的進(jìn)程Proc（）的可達(dá)空間為整個訪問控制系統(tǒng)的可達(dá)空間。

5.2分析

安全性分析主要討論訪問許可泄露問題，其主要目標(biāo)在于對給定的主體、客體和權(quán)限，該主體能否最終獲得對該客體的訪問權(quán)限。在UCON中，主體對客體的訪問權(quán)限的許可完全取決于當(dāng)前狀態(tài)下主體與客體屬性值，如在實(shí)例11中如果讀者1擁有的expense為3，則其不能閱讀書b0，如果增加到6，則可以閱讀書b0。UCON的主要優(yōu)點(diǎn)在于訪問許可的執(zhí)行會引起主客體屬性值的變化，而正是這種變化給UCON模型的安全性分析帶來了很大的困難。文獻(xiàn)［19］將安全性分成簡單安全性、簡單可用性、約束安全性、活性與包含性5類，本節(jié)將給出PAT框架下5種屬性的分析方法。

簡單安全性是指是否存在一個可達(dá)狀態(tài)，使該狀態(tài)下指定的主體能夠獲取指定客體的訪問權(quán)限。假設(shè)謂詞P1&&…&&Pn用來決策指定主體能否獲取指定客體的訪問權(quán)限，可通過可達(dá)性檢測完成安全性分析：斷言#assert reaches P1&&…&&Pn為真，則說明權(quán)限被許可，否則說明權(quán)限未被許可。

簡單可用性是指在每個可達(dá)狀態(tài)下，指定的主體是否能夠獲取指定的客體的訪問權(quán)限。

假設(shè)謂詞P1&&…&&Pn用來決策指定主體能否獲取指定客體的訪問權(quán)限，可通過驗(yàn)證LTL屬性［］（P1&&…&&P2）來實(shí)現(xiàn)簡單可用性的驗(yàn)證：此屬性成立說明在每個可達(dá)狀態(tài)下謂詞P1&&…&&Pn為真，即在每個可達(dá)狀態(tài)下訪問得到了許可，反之說明簡單可用性不成立。

限界安全性是指在每個可達(dá)狀態(tài)下，對于給定的客體，可獲取該客體訪問權(quán)限的主體是否在指定的主體范圍內(nèi)。對于主體i，客體j，訪問訪問權(quán)限r(nóng)，定義謂詞Predicate.i.j.r表示訪問權(quán)限的決策項(xiàng)。不失一般性，假設(shè)有m個主體，編號分別為0，…，m-1，1個客體，編號為0，一種訪問權(quán)限，編號為0，指定的主體范圍是｛0，…，k｝，指定的客體是0，限界安全性可以用過驗(yàn)證LTL屬性［］！（Predicate.（k+1）.0.0||…||Predicate.（m-1）.0.0）來實(shí)現(xiàn)。該屬性為真說明在任一可達(dá)狀態(tài)下謂詞Predicate.（k+1）.0.0到 Predicate.（m-1）.0.0均為假，即主體k+1到主體m-1都沒有獲取相應(yīng)的權(quán)限，反之限界安全性不成立。

活性是指在任一可達(dá)狀態(tài)下至少有一個主體能夠獲得對某個客體的訪問權(quán)限?；钚缘尿?yàn)證等于驗(yàn)證是否存在一個可達(dá)狀態(tài)，使得沒有一個用于訪問決策判斷的謂詞為真，因此可以通過可達(dá)性檢測來驗(yàn)證活性。假設(shè)有m個主體，n個客體，k個權(quán)限。對于主體i，客體j，訪問訪問權(quán)限 r，定義謂詞 Predicate.i.j.r表示訪問權(quán)限的決策項(xiàng)，斷言#assert reaches為真，則說明存在一個可達(dá)狀態(tài)，使沒有一個決策謂詞為真，即活性不成立，反之成立。

包含性是指在任一可達(dá)狀態(tài)下對某個客體擁有某種訪問權(quán)限的主體是否也擁有對另外一個客體的另外一種權(quán)限。不失一般性，假設(shè)有2個客體，編號分別為0和1，有2種權(quán)限，編號分別為 0和 1。設(shè)計(jì)斷言#assert reaches該斷言為真，則說明存在一個可達(dá)狀態(tài)，該狀態(tài)下Predicate.i.0.0-> Predicate.i.0.1為假，即對指定的客體擁有某種訪問權(quán)限的主體沒有擁有另外一種權(quán)限。斷言為假，說明包含性成立。

5.3完全性與相容性

完全性與相容性是訪問控制系統(tǒng)中另外2個重要的基本問題。關(guān)于UCON的完全性和沖突性目前還未見任何相關(guān)的工作，文獻(xiàn)［10］也將這2個問題列為UCON未來需要解決的問題，本節(jié)將對如何利用PAT完成2個屬性的驗(yàn)證展開系統(tǒng)的討論。

完全性是指對于主體發(fā)出的任意請求，系統(tǒng)必須給出準(zhǔn)確的回應(yīng)，要么同意，要么許可。UCON采取授權(quán)、義務(wù)和條件3種因素共同決策訪問的許可，當(dāng)3個因素都成立時，訪問得到許可，否則拒絕。對UCON而言，只有一種情況會造成控制策略的不完全，即遺漏了某個主體對某個客體發(fā)出某種權(quán)限的訪問請求的TCSP#規(guī)范。因此UCON的不完全性可以歸結(jié)為：對于任意的主體i，任意的客體j，任意的權(quán)限r(nóng)，是否進(jìn)行了相應(yīng)的TCSP#規(guī)范描述。可以通過驗(yàn)證LTL性質(zhì)［］！tryaccess.i.j.r達(dá)到驗(yàn)證完全性的目的：如果存在主體i，客體j，權(quán)限r(nóng)使［］！tryaccess.i.j.r為真，則說明UCON是不完全的，否則是完全的。

不相容性是指對于某個訪問，存在不少于 2個訪問控制決策，依據(jù)其中的一個規(guī)則訪問得到許可，依據(jù)另外一條規(guī)則，則訪問被拒絕。2個訪問控制決策是相容的，意味著對于任意一個訪問請求，決策的結(jié)果應(yīng)該是一致的，換句話講從決策的結(jié)果判斷，2個進(jìn)程應(yīng)該是等價的，為此建立如下相容性檢測過程。

Procedure 2相容性檢測。

Step1依據(jù) Type-1并發(fā)對第一個訪問控制規(guī)則建立TCSP#規(guī)范，記為Procedure_1（i，j，r）。

Step2依據(jù) Type-1并發(fā)對第二個訪問控制規(guī)則建立TCSP#規(guī)范，記為Procedure_2（i，j，r）。

Step3建立進(jìn)程P（）用以對變量進(jìn)行初始化。

Step4建立進(jìn)程 Proc_1=P（）；Procedure_1（i，j，r）。

Step5建立進(jìn)程 Proc_2=P（）；Procedure_2（i，j，r）。

Step6建立斷言#assert Proc_1 refines Proc_2。

Step7建立斷言#assert Proc_2 refines Proc_1。

Step8驗(yàn)證2個斷言是否成立：都成立說明2個規(guī)則相容，否則說明不相容。

實(shí)例13在一個醫(yī)院的信息管系統(tǒng)中有3個用戶組：醫(yī)生、護(hù)士、主治人員，其中主治人員包括主治醫(yī)生和主治護(hù)士2個子角色。訪問控制策略主要有3個［20］。

Policy1醫(yī)生不能對病人進(jìn)行查房。

Policy2主治醫(yī)生可以對病人進(jìn)行查房。

Policy3醫(yī)生可以查閱任何病人的醫(yī)療記錄。

現(xiàn)在驗(yàn)證Policy 1與Policy 2的相容性。初始假設(shè)：2個醫(yī)生，編號分別為0和1；2個護(hù)士，編號分別為0和1；2個病人，編號分別為0和1；0號病人的主治醫(yī)生是0，主治護(hù)士是0，1號病人的主治醫(yī)生是1，主治護(hù)士是1。

定義數(shù)組S［2］表示主體屬性：s［i］=1，表示i是醫(yī)生。定義數(shù)組o［2］表示客體屬性：o［i］=j，表示j是i號病人的主治醫(yī)生。

Step1依據(jù) Type-1 并發(fā) 對 Rule1建立TCSP#規(guī)范。

Procedure_1（i，j，r）=tryaccess.i.j.r->if（s［i］==1）｛denyaccess.i.j.r->Skip｝else｛permitaccess.i.j.r-> doaccess.i.j.r->end.i.j.r->Skip｝

Step2依據(jù)Type-1并發(fā)對Rule2建立TCSP#規(guī)范。

Procedure_2（i，j，r）=tryaccess.i.j.r->if（o［j］==i）｛permitaccess.i.j.r->doaccess.i.j.r->end.i.j.r->Skip｝else｛denyaccess.i.j.r->Skip｝

Step3建立進(jìn)程P（）用以對變量進(jìn)行初始化。

P（）=initialization｛s［0］=1；s［1］=1；o［0］=0；o［1］=1 ｝->Skip

Step4建立進(jìn)程 Proc_1=P（）；Procedure_1（i，j，r）。

Step5建立進(jìn)程 Proc_2=P（）；Procedure_2（i，j，r）。

Step6建立斷言#assert Proc_1 refines Proc_2。

Step7建立斷言#assert Proc_2 refines Proc_1。

Step8驗(yàn)證2個斷言是否成立，都成立說明2個規(guī)則相容，否則說明不相容。

利用PAT工具，驗(yàn)證發(fā)現(xiàn)這2個斷言都不成立，因此Policy 1和Policy 2是不相容的。

6　會議論文評審系統(tǒng)

考察一個會議論文評審系統(tǒng)［21］。該系統(tǒng)包含的對象是評審專家與準(zhǔn)備評審的論文。評審系統(tǒng)遵循如下訪問控制策略。

Policy1程序委員會主席為每個評審專家分配評審的論文，每篇論文的評審專家為2人。

Policy2對于任意一篇論文 p，如果在當(dāng)前系統(tǒng)中p沒有指派給評審專家a評審，則a可以查看評審專家b對論文的評審意見。

Policy3如果論文p被同時指派給了評審專家a與b評審，只有當(dāng)a完成審稿后才能查看b對論文的評審意見。

Policy4如果論文p已經(jīng)被指派給評審專家a評審，在沒有完成審稿之前a隨時可以終止本次審稿。

Policy5如果論文p已經(jīng)被指派給評審專家a評審，在a沒有完成審稿之前，程序委員會主席可隨時撤銷a對p的審稿權(quán)。

制定這些控制策略的主要目的是阻止評審專家的意見受其他評審專家的影響。Policy 1可以設(shè)計(jì)一個初始化進(jìn)程來完成。Policy 2 和Policy 3沒有改變?nèi)魏沃黧w與客體屬性，且必須滿足某個條件才能查看其他評審專家提交的評審意見，因此對應(yīng)的策略控制核心模型為preA0。Policy 4改變了主體的屬性，且發(fā)生在訪問請求得到許可之后、執(zhí)行之前，因此對應(yīng)的策略控制執(zhí)行模型為preA1。Policy 5改變了客體的屬性，且發(fā)生在訪問請求得到許可之后、執(zhí)行之前，因此對應(yīng)的策略控制執(zhí)行模型為preA1。具體分析的安全性如下。

1）簡單安全性：某個評審專家最終能否獲取某篇論文的評審權(quán)。

2）簡單可用性：任意時刻某個評審專家能否獲取某篇論文的評審權(quán)。

3）限界安全性：任意時刻獲取某篇論文評審權(quán)的主體是否在指定的主體范圍內(nèi)。

4）活性：在任意可達(dá)狀態(tài)下至少有一個評審專家能夠獲得對某篇論文的訪問權(quán)限。

5）包含性：任意時刻某個評審專家擁有對某篇論文的評審權(quán)是否也同時擁有拒絕某篇論文評審的權(quán)利。

6）完全性：任意時刻某個評審專家對某篇論文發(fā)出任何訪問請求都會得到響應(yīng)。

7）相容性：任意時刻某個評審專家對某篇論文發(fā)出任何訪問請求，不會出現(xiàn)既得到許可又得到拒絕的響應(yīng)。

表1　不同評審專家和論文數(shù)量情況下的實(shí)驗(yàn)結(jié)果

除了上述簡單的安全屬性外，還需考察公平性：評審專家對論文的評審不受其他評審意見的影響，即任意評審專家在提交某篇論文的評審意見前沒有看到其他評審專家對該論文的評審的意見。

現(xiàn)在通過實(shí)驗(yàn)結(jié)果來評估算法的性能。所有的實(shí)驗(yàn)均基于 PAT3.5.1完成，實(shí)驗(yàn)環(huán)境為：Windows 8操作系統(tǒng)，2.83 GHz Intel Q9550 CPU，4 GB內(nèi)存。運(yùn)行時間的上限設(shè)置為60 min。表1收集了不同評審專家和論文數(shù)量情況下的實(shí)驗(yàn)結(jié)果。在表1中，用一個二元組（i，j）表示規(guī)模，其中i表示評審專家的人數(shù)，j表示需要評審的論文數(shù)。

從表1的數(shù)據(jù)可以看出，除了活性和公平性，其他屬性的驗(yàn)證時間是完全可以接受的，內(nèi)存空間的使用是非常有限的。因此從時空效率的角度而言，使用PAT來完成UCON的安全性分析是完全可行的。

7　結(jié)束語

本文依托于先進(jìn)的模型檢測工具PAT，利用PAT的建模語言TCSP#建立了所有UCON核模型的規(guī)范，以及一般化UCON模型的規(guī)范機(jī)制，對復(fù)雜的使用會話場景，如并發(fā)、時間控制與非確定性也建立了一套規(guī)范機(jī)制?？蛇_(dá)空間的計(jì)算是分析UCON安全性的基礎(chǔ)，本文提出了一種進(jìn)程代數(shù)構(gòu)造機(jī)制，使該進(jìn)程代數(shù)可以刻畫任意時刻任意主體對任意客體放出任意訪問請求，因此該進(jìn)程代數(shù)的狀態(tài)空間就是訪問控制系統(tǒng)的可達(dá)空間?；诳蛇_(dá)空間，給出了安全性分析技術(shù)，基于進(jìn)程代數(shù)的等價關(guān)系，提出了控制策略沖突性檢測方法?？偠灾?，在PAT下從UCON的規(guī)約到安全性分析，提出了一套系統(tǒng)的解決方案。

在第6節(jié)的實(shí)例研究中，發(fā)現(xiàn)隨著主客體數(shù)量的增長，可達(dá)空間的增長非常快，這為大規(guī)模UCON的驗(yàn)證帶來了挑戰(zhàn)，未來的主要工作是如何應(yīng)對狀態(tài)空間增長過快的問題。

［1］PFLEEGER C P，PFLEEGER S L. Security in computing［M］. Prentice Hall Professional Technical Reference，2002.

［2］SANDHU R S，COYNE E J，F(xiàn)EINSTEIN H L，et al. Role-based access control models［J］. Computer，1996，29（2）：38-47.

［3］FERRAIOLO D F，SANDHU R，GAVRILA S，et al. Proposed NIST standard for role-based access control［J］. ACM Transactions on Information and System Security（TISSEC），2001，4（3）：224-274.

［4］PARK J，SANDHU R. The UCON ABC usage control model［J］. ACM Transactions on Information and System Security（TISSEC），2004，7（1）：128-174.

［5］ZHANG X，PARISI-PRESICCE F，SANDHU R，et al. Formal model and policy specification of usage control［J］. ACM Transactions on Information and System Security（TISSEC），2005，8（4）：351-387.

［6］ZHANG X. Formal model and analysis of usage control［D］. Fairfax County，Virgina：George Mason University，2006.

［7］JANICKE H，CAU A，ZEDAN H. A note on the formalisation of UCON［C］//The 12th ACM Symposium on Access Control Models and Technologies. c2007：163-168.

［8］MARTINELLI F. A model for usage control in GRID systems［C］//The Third International Conference on Security and Privacy in Communications Networks and the Workshops. c2007：520-520

［9］JAGADEESAN R，MARRERO W，PITCHER C，et al. Timed constraint programming：a declarative approach to usage control［C］//The 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. c2005：164-175.

［10］LAZOUSKI A，MARTINELLI F，MORI P. Usage control in computer security：a survey［J］. Computer Science Review，2010，4（2）：81-99.

［11］ZHANG X，SANDHU R，PARISI-PRESICCE F. Safety analysis of usage control authorization models［C］//The 2006 ACM Symposium on Information，Computer and Communications Security. c2006，6：243-254.

［12］RAJKUMAR P V，GHOSH S K，DASGUPTA P. Concurrent usage control implementation verification using the SPIN model checker［C］//The Third International，CNSA 2010，Chennai，India. Berlin Heidelberg Springer. c2010：214-223.

［13］HOLZMANN G J. The model checker SPIN［J］. IEEE Transactions on Software Engineering，1997，23（5）：279-295.

［14］SUN J，LIU Y，DONG J S，et al. PAT：towards flexible verification under fairness［C］//The 21st International Conference on Computer Aided Verification. c2009：709-714.

［15］SUN J，LIU Y，DONG J S，et al. Modeling and verifying hierarchical real-time systems using stateful timed csp［J］. ACM Transactions on Software Engineering and Methodology（TOSEM），2013，22（1）：139-176.

［16］VARDI M Y. An automata-theoretic approach to linear temporal logic［M］//Logics for concurrency. Berlin Heidelberg：Springer，1996.238-266.

［17］MCLEAN J. A comment on the ‘basic security theorem'of bell and LaPadula［J］. Information Processing Letters，1985，20（2）：67-70.

［18］KATT B，HAFNER M，ZHANG X. A usage control policy specification with petri nets［C］//The 5th International Conference on Collaborative Computing：Networking，Applications and Worksharing. c2009：1-8.

［19］LI N，TRIPUNITARA M V. Security analysis in role-based access control［J］. ACM Transactions on Information and System Security（TISSEC），2006，9（4）：391-420.

［20］ADI K，BOUZIDA Y，HATTAK I，et al. Typing for conflict detection in access control policies［M］//E-technologies：Innovation in An Open World. Berlin Heidelberg：Springer，2009：212-226.

［21］ZHANG N，RYAN M，GUELEV D P. Synthesising verified access control systems through model checking［J］. Journal of Computer Security，2008，16（1）：1-61.

［22］LAMPORT L. The temporal logic of actions［J］. ACM Transactions on Programming Languages and Systems（TOPLAS），1994，16（3）：872-923.

Formal specification and security verification of usage control model based on PAT

ZHOU Cong-hua，CHEN Wei-he，LIU Zhi-feng

（School of Computer Science and Telecommunication Engineering，Jiangsu University，Zhenjiang 212013，China）

Usage control（UCON）is an access control model to enforce digital resources protection in highly distributed，heterogeneous network computing environment. Firstly，each core model of UCON was specified formally with TCSP#，and a combination specification mechanism was proposed for general UCON. Secondly，as the basis of the security analysis，the concepts and calculation method of the reachable space were given. Various combination mechanisms of processes based on single-session was presented to achieve formal specifications of complex concurrent sessions，timings and nondeterminism. Then the reachable space of combined processes was the desired space. Finally，the security analysis method based on the reachable space and the conflict analysis of access control policies based on the equivalent checking in process algebras were proposed for UCON model. All the proposed work had been formal checked in PAT. The experiment result shows that the proposed approaches are feasible，and PAT is a really great tool for the systematic formal specification and security analysis of UCON.

UCON，formal specification，security analysis，model checking

1　引言

現(xiàn)今社會，信息技術(shù)持續(xù)的創(chuàng)新促使各種移動設(shè)備如智能手環(huán)、移動電話、PAD等成為人們?nèi)粘Ｉ畈豢苫蛉钡男畔a(chǎn)品，進(jìn)而使對數(shù)字信息的訪問變得無處不在，訪問環(huán)境也從封閉系統(tǒng)轉(zhuǎn)變?yōu)榉植际?、網(wǎng)絡(luò)化的計(jì)算環(huán)境。在這種無處不在的計(jì)算環(huán)境下，傳統(tǒng)的訪問控制，如自主訪問控制DAC［1］、強(qiáng)制訪問控制MAC［1］與角色訪問控制 RBAC［2，3］已經(jīng)不再適用。Park和 Sandhu［4］在2002年首次提出了UCON模型，目的在于實(shí)現(xiàn)無處不在的開放式計(jì)算環(huán)境下對信息的合法訪問。

The National Natural Science Foundation of China（No.61300228）

TP309.7

A

10.11959/j.issn.2096-109x.2016.00038

2016-02-12；

2016-03-05。通信作者：周從華，chzhou@ujs.edu.cn

國家自然科學(xué)基金資助項(xiàng)目（No.61300228）

周從華（1978-），男，江蘇鹽城人，博士，江蘇大學(xué)副教授，主要研究方向?yàn)樵L問控制、形式化方法。

陳偉鶴（1974-），男，江蘇丹陽人，博士，江蘇大學(xué)副教授，主要研究方向?yàn)樵L問控制、數(shù)據(jù)挖掘。

劉志鋒（1981-），男，江蘇無錫人，博士，江蘇大學(xué)副教授，主要研究方向?yàn)樵L問控制、形式化方法。