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

周從華，陳偉鶴，劉志鋒

（江蘇大學計算機科學與通信工程學院，江蘇 鎮江 212013）

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

周從華，陳偉鶴，劉志鋒

（江蘇大學計算機科學與通信工程學院，江蘇 鎮江 212013）

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

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

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

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

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

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

2　使用控制UCON

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

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

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

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

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

3　UCON的TCSP#規范

依據無處不在計算環境下訪問控制的執行流程，可以定義如下9個原子事件。

1）tryaccess.s.o.r：主體s對客體o產生一個權限為r的訪問請求。

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

3）denyaccess.s.o.r：訪問請求 tryaccess.s.o.r被系統拒絕。

4）doaccess.s.o.r：主體s對客體o執行權限為r的訪問。

5）revokeaccess.s.o.r：系統撤銷主體s對客體o正在執行的權限為r的訪問。

6）endaccess.s.o.r：主體s主動結束對客體o的權限為r的訪問。

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

8）onupdate.s.o.r：在訪問的過程中由系統來更新主客體的屬性，這種更新操作在訪問過程中可以重復進行。

9）postupdate.s.o.r：在訪問結束后由系統更新主客體的屬性。

3.1授權核模型的規約

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

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

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

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

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

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

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

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

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

3.1.1核模型preA0

在preA0中授權決策由系統執行，且發生在訪問之前，同時主體和客體的屬性在訪問全程中沒有任何變化。利用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是建立在主體和客體屬性上的授權謂詞。當該謂詞為真時，訪問得到許可，并開始執行，否則訪問被系統予以拒絕。為了區分不同的訪問進程，在進程的命名上，preA0表示決策和屬性更新的類型，S表示具有某種共同特性的主體集，如STUDENT表示由學生形成的主體的集合，O表示具有某種共同特性的客體集，如 FILE表示由文件形成的集合，R表示權限的類型，如READ表示讀權限。為了方便讀者體會如何使用TCSP#建模以及與以往形式化規范工作的區別，本文的實例盡量選自文獻［5］。

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

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

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

第一種方式的 TCSP#規范描述如下，其中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#規范描述如下。

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的主要不同在于在訪問控制實施之前主客體的屬性可能會被更新。一般情況下，更新操作發生在主體發出訪問請求且請求得到許可之后。利用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的更新。

實例 2在一個按次計費的數字版權保護系統中，主體擁有屬性credit，表示擁有的存款，客體擁有屬性value，表示每次訪問的代價。當主體的credit超過客體的value時，主體可以對客體執行讀的訪問。在訪問開始前，主體的存款 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中，授權決策由系統在訪問之前檢測，且在訪問過程中會有多個屬性值被更新。利用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中，授權決策由系統在訪問之前檢測，且在訪問結束后會有多個屬性值被更新。利用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｝

實例 3在一個基于會員的數字版權管理系統中，讀者擁有屬性expense和readingGroup，書擁有屬性readingGroup和readingCost。如果讀者和書屬于同一個閱讀組，則讀者可以閱讀此書，同時閱讀結束后讀者的閱讀費用在原 expense的基礎上增加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

在授權決策由系統在訪問之前檢測的模式下，訪問請求得到許可后將不再進行安全檢查。在模型onA0中，授權決策將被重復檢測，一旦檢測到授權謂詞真值為假，系統立即撤銷此次訪問。在訪問的過程中，主體隨時可能結束訪問，引入事件continue.s.o.r表示主體繼續訪問，引入事件nocontinue.s.o.r表示主體主動結束訪問。利用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｝

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

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中主客體的屬性在訪問過程中重復被更新。

利用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中主客體的屬性在訪問結束后進行更新。利用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｝

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

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

2）o_accessing_number表示訪問客體o的主體的數量。

3）sys_clock表示系統時間，為系統屬性。

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

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

現在以最早開始時間為撤銷策略為例。因為屬性的更新發生在訪問開始前和訪問結束后，所以，整體的使用控制策略定義為 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（?。╫_ 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義務核模型的規約

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

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

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

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

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

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

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

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

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

3.2.1核模型preB0

preB0規定只有當所有的義務事件完成后，訪問才能被許可。以一個義務事件ob為例來說明preB0對應的訪問控制流程，主體可以執行義務，也可以不執行，引入事件noob表示主體沒有執行義務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）

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

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規定只有當所有的義務事件完成后，訪問才能被許可，且在訪問開始之前需要更新主客體的屬性。利用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規定只有當所有的義務事件完成后，訪問才能被許可，且在訪問過程中更新主客體的屬性。利用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規定只有當所有的義務事件完成后，訪問才能被許可，且在訪問結束后更新主客體的屬性。利用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）

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

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規定主體必須在訪問控制的過程中重復執行義務事件，否則訪問將被取消，且在整個訪問過程中無需更新主客體的屬性。利用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）

實例 8為了使用在線服務，廣告標語必須在客戶端打開，否則服務就失效。該控制策略的TCSP#規范表示如下。

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規定主體必須在訪問控制的過程中重復執行義務事件，否則訪問將被取消，且在訪問開始前更新主客體的屬性。利用 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規定主體必須在訪問控制的過程中重復執行義務事件，否則訪問將被取消，且在訪問過程中重復更新主客體的屬性。利用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規定主體必須在訪問控制的過程中重復執行義務事件，否則訪問將被取消，且在訪問結束或者撤銷后更新主客體的屬性。利用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）

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

此實例中義務的執行是有條件的，即只有當在線時間達到30 min時才必須執行點擊廣告的事件，因此在重復檢測的過程中需要加入條件進行判斷。以下是該控制流程的TCSP#規范。

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條件核模型的規約

條件構件是面向環境和系統的決策因素，條件謂詞用于估算當前的環境和系統狀態。與授權、義務不同，條件不能改變主客體的屬性?；跅l件謂詞估算的時間點的不同，條件核模型可以分為預條件和在線條件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中條件謂詞在訪問的過程中不斷被檢測，如果謂詞真值為真，則繼續訪問，否則立即撤銷當前的訪問。此外在訪問整個過程中沒有任何的主客體屬性被更新。利用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｝

實例 10訪問控制策略定義一個值日班的職員（角色為dayshifter）僅僅在白天能夠訪問對象、定義currenttime為系統屬性，表示當前時間。該策略是 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　并發、時間約束、非確定性

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

4.1并發

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

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

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

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

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

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并發：上次訪問結束后主體可以繼續對同一客體發出多次相同的訪問請求。

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

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 并發與Type-1并發的主要區別在于，將preA1_S_O_R_Type_1（i，j，r）中所有Skip事件替換為preA1_S_O_R_Type_2（i，j，r）。依據TCSP#的語義解釋，當事件end或者denyaccess執行結束后，按照 preA1_S_O_R_Type_2（i，j，r）的規范重新開始運行，從而實現了新一輪次的訪問。

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

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

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并發：同一時間主體可以對客體發出多次相同的訪問。

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

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｝

定義進程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）。

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

5）Type-5并發：在一段時間內主體可以對不同的客體產生訪問請求。

在TCSP#中多進程之間的交互意味著在任意時刻可從多進程中任意選擇一個進程執行，利用交互算子|||定義進程 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個子進程中選擇一個進程執行，從而達到主體對不同客體的訪問。

6）Type-6并發：在一段時間內不同主體可以對相同的客體產生訪問請求。

與Type-5并發類似，定義進程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并發：同一時間主體可以對不同的客體產生訪問請求。

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

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｝

定義進程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）必須同時執行事件 tryaccess，然后獨立運行，從而實現了同一時間點主體對不同客體產生訪問的請求。

8）Type-8并發：同一時間不同主體可以對相同的客體產生訪問請求。

與Type-7并發類似，定義進程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并發：在一段時間內不同主體可以對不同的客體產生訪問請求。

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）。|||表示進程之間的交互執行，因此上述進程表示m個主體在一段時間內對n個客體產生了訪問請求。

10）Type-10并發：同一時間不同主體可以對不同的客體產生訪問請求。

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）。在上述進程中所有進程必須同時執行事件 tryaccess，從而實現同一時間不同主體可以對不同客體產生訪問請求。

11）Type-11并發：在一段時間內不同主體可以對不同的客體產生多次訪問請求。

定義進程 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）實現了對同一客體的多次訪問請求，|||實現了訪問之間的交互。

12）Type-12并發：與系統環境的交互。

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

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

4.2時間控制

在UCON中當主體發出訪問請求后，系統必須在一段時間內進行響應，客體也必須在一定的時間內完成義務事件的執行。例如，在一個在線電子商務中，顧客必須點擊同意購買協議的按鈕才能繼續購物。這種點擊必須有時間限制，不可能為消費者等待無窮時間，如可以設置如果在 5 min內不點擊就撤銷此次訪問請求。為此考察以下幾種時間約束的TCSP#規范。

1）Type-1時間控制：請求發出后，必須在某段時間內得到響應，否則繼續發送訪問請求。

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

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］表示主體執行完事件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 ｝在d個時間單元內執行了某個事件，則繼續按照此進程的規范執行，否則執行進程denyaccess.s.o.r->preA0_S_O_R_Type-1_Timing（s，o，r）。

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

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

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］表示系統執行完事件 permitaccess.s.o.r后，如果進程doaccess.s.o.r->end.s.o.r->Skip在d個時間單元內執行了事件 doaccess.s.o.r，則繼續按照此進程的規范執行，否則執行進程denyaccess.s.o.r -> preA0_S_O_R_ Type_2_Timing（s，o，r）。

3）Type-3時間控制：義務的執行必須在某個時間段內完成，否則撤銷此次訪問。

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

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中，進程ob.s.o.r->doaccess.s.o.r->end.s.o.r的第一個事件ob.s.o.r必須在時間 d內執行，否則執行進程denyaccess.s.o.r->Skip。

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

策略1套接字必須在發送數據前打開。

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

策略3每個用戶發送數據包的時間不能超過10 min。

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

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中的典型情況，應用TCSP#成功刻畫了這些場景，充分說明了TCSP#刻畫時間控制的能力。

4.3非確定性

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

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

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

5　安全性分析

安全性分析是訪問控制系統中最基礎最重要的問題，其主要目標是是判斷主體能否最終獲得對客體的訪問權限。對于傳統訪問控制模型，主要通過遍歷控制系統的可達狀態空間進行安全性分析。這種方法也適用于UCON。

5.1全局可達空間的構造

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

構造進程代數的關鍵在于必須能夠表達任意時刻任意主體對任意客體發送任意的訪問請求。在給出構造方法之前，先做一些假設：主體數目為m，客體數目為n，訪問權限只有r一種。具體的進程構造過程如下。

Procedure 1面向可達空間計算的進程代數的構造。

Step1構造初始化進程定義進程 P（）= initialization｛…｝->Skip用于對變量進行初始化。

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

Step3依據Type-2 并發，在Proc_1（i，j，r）的基礎上構造上次訪問結束后主體可以繼續對同一客體發出訪問請求的流程，記為Proc_2（i，j，r）。

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

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

Step6構造任一主體對任一客體的交互訪問。定義進程Proc_5（）=Proc_4（0）|||…|||Proc_4（m-1）。

Step7定義進程Proc（）=P（）；Proc_5（）。

定理1Procedure 1構造出的進程Proc（）的可達空間為整個訪問控制系統的可達空間。

5.2分析

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

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

簡單可用性是指在每個可達狀態下，指定的主體是否能夠獲取指定的客體的訪問權限。

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

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

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

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

5.3完全性與相容性

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

完全性是指對于主體發出的任意請求，系統必須給出準確的回應，要么同意，要么許可。UCON采取授權、義務和條件3種因素共同決策訪問的許可，當3個因素都成立時，訪問得到許可，否則拒絕。對UCON而言，只有一種情況會造成控制策略的不完全，即遺漏了某個主體對某個客體發出某種權限的訪問請求的TCSP#規范。因此UCON的不完全性可以歸結為：對于任意的主體i，任意的客體j，任意的權限r，是否進行了相應的TCSP#規范描述?？梢酝ㄟ^驗證LTL性質［］！tryaccess.i.j.r達到驗證完全性的目的：如果存在主體i，客體j，權限r使［］！tryaccess.i.j.r為真，則說明UCON是不完全的，否則是完全的。

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

Procedure 2相容性檢測。

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

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

Step3建立進程P（）用以對變量進行初始化。

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

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

Step6建立斷言#assert Proc_1 refines Proc_2。

Step7建立斷言#assert Proc_2 refines Proc_1。

Step8驗證2個斷言是否成立：都成立說明2個規則相容，否則說明不相容。

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

Policy1醫生不能對病人進行查房。

Policy2主治醫生可以對病人進行查房。

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

現在驗證Policy 1與Policy 2的相容性。初始假設：2個醫生，編號分別為0和1；2個護士，編號分別為0和1；2個病人，編號分別為0和1；0號病人的主治醫生是0，主治護士是0，1號病人的主治醫生是1，主治護士是1。

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

Step1依據 Type-1 并發 對 Rule1建立TCSP#規范。

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依據Type-1并發對Rule2建立TCSP#規范。

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建立進程P（）用以對變量進行初始化。

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

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

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

Step6建立斷言#assert Proc_1 refines Proc_2。

Step7建立斷言#assert Proc_2 refines Proc_1。

Step8驗證2個斷言是否成立，都成立說明2個規則相容，否則說明不相容。

利用PAT工具，驗證發現這2個斷言都不成立，因此Policy 1和Policy 2是不相容的。

6　會議論文評審系統

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

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

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

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

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

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

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

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

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

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

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

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

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

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

表1　不同評審專家和論文數量情況下的實驗結果

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

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

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

7　結束語

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

在第6節的實例研究中，發現隨著主客體數量的增長，可達空間的增長非常快，這為大規模UCON的驗證帶來了挑戰，未來的主要工作是如何應對狀態空間增長過快的問題。

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

［2］SANDHU R S，COYNE E J，FEINSTEIN 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　引言

現今社會，信息技術持續的創新促使各種移動設備如智能手環、移動電話、PAD等成為人們日常生活不可或缺的信息產品，進而使對數字信息的訪問變得無處不在，訪問環境也從封閉系統轉變為分布式、網絡化的計算環境。在這種無處不在的計算環境下，傳統的訪問控制，如自主訪問控制DAC［1］、強制訪問控制MAC［1］與角色訪問控制 RBAC［2，3］已經不再適用。Park和 Sandhu［4］在2002年首次提出了UCON模型，目的在于實現無處不在的開放式計算環境下對信息的合法訪問。

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

國家自然科學基金資助項目（No.61300228）

周從華（1978-），男，江蘇鹽城人，博士，江蘇大學副教授，主要研究方向為訪問控制、形式化方法。

陳偉鶴（1974-），男，江蘇丹陽人，博士，江蘇大學副教授，主要研究方向為訪問控制、數據挖掘。

劉志鋒（1981-），男，江蘇無錫人，博士，江蘇大學副教授，主要研究方向為訪問控制、形式化方法。