安全協(xié)議是用來實施安全功能的一種重要的安全技術(shù),，是許多分布式系統(tǒng)安全的基礎(chǔ),。設(shè)計一種正確的、符合安全目標,、沒有冗余的安全協(xié)議,，是一件非常困難的事情。為此,，人們越來越多地關(guān)注形式化方法,，期望建立一套完整成熟的理論和技術(shù)，并將該理論和技術(shù)用于實踐中,，設(shè)計,、驗證和改進安全協(xié)議。
　　安全協(xié)議設(shè)計和分析的困難性是由多方面因素造成的,。其中最先遇到的問題就是安全問題本身的微妙性^[1],。即對于一個表面上很簡單的問題，卻有著許多不同的觀點,。如果采用自然語言來描述該安全問題,，則難免會出現(xiàn)不同的理解，從而對安全問題的定義出現(xiàn)模糊性和不確定性,。所以,，需要用一種安全協(xié)議的形式化需求語言來確切地描述安全需求。
　　目前,，已經(jīng)開發(fā)出一種安全協(xié)議的形式化需求語言^[4],。但這種語言還不夠成熟，仍有以下需要改進的地方：
　　(1)該語言比較簡單,，語義不夠豐富,，對于許多安全需求,，例如認證、授權(quán),、公平性等都無法描述,。
　　(2)不適合于描述復雜的分布式系統(tǒng)，特別是網(wǎng)格系統(tǒng),。該語言一般適用于兩個用戶的系統(tǒng),，對于多用戶的復雜分布式系統(tǒng)，該語言的描述非常繁瑣,，甚至無能為力,。
　　(3)該語言還不夠嚴謹，有些定義是冗余的,，有些定義是模糊的,，不夠清晰。以上這些問題造成了該語言在實際應用中的局限性,，無法充分地發(fā)揮作用,。本文在以上幾個方面作了改進，解決了以上幾個方面存在的不足,，使該語言更加成熟,。這種改進的安全協(xié)議的形式化需求語言主要是針對網(wǎng)格這一典型的復雜分布式系統(tǒng)的需求而設(shè)計的。將本語言簡化后,，還可以適用于簡單的分布式系統(tǒng),。
1 改進的安全協(xié)議形式化需求語言
　　本語言由有限個常量項、變量項,、n元函數(shù)、n元動作,、原子謂詞公式,、復合公式、邏輯連接符(包括∧,、∨,、┐、→,、等)和時態(tài)操作符θ^[5]等組成,。時態(tài)操作符θ表示某個動作發(fā)生在過去的某個時刻。
　　復雜的分布式系統(tǒng)存在用戶量大的特點,，為了適應這個特點引入了集合^[6],，用來表達組的概念，描述組內(nèi)的成員在某個方面具有某項共同的性質(zhì)和某種共同的行為,。這樣可以使本語言更加簡潔,。
　　(1)主體x：是一個有限集,，集合中的元素是網(wǎng)格中的用戶，或者是用戶的代理,。其中包括誠實用戶,、攻擊者用戶和可信第三方(誠實的、能夠協(xié)助運算順利完成的第三方,，例如網(wǎng)格服務管理者,、協(xié)同計算服務管理者、證書認證中心等)及其代理,?？占?覫代表集合中不含有用戶，全集E表示集合中含有全部用戶,。最常見的主體是由一個用戶組成的集合,。對主體的兩種運算(集合的并集、集合的減法,，即組內(nèi)用戶數(shù)目的增多與減少)構(gòu)成了主體空間X：
　　x₁∪x₂∈X
　　x₁-x₂∈X
　　(2)消息m：是通信的內(nèi)容,。有三種原子消息：主體標識、密鑰和新鮮數(shù)(包括隨機數(shù)和時間戳),。對原子消息和有效消息(有效信息是指通信中最終要傳輸?shù)?、包含有某些實際信息的消息，以上三種原子消息,，最終都是為了傳輸有效消息服務)的四種運算(合成,、分解、加密和解密)構(gòu)成了消息空間M：
　　
　　其中,，°表示級聯(lián),，k與k^-1為互逆密鑰。
　　(3)函數(shù)：定義從消息空間M到主體空間X和從消息空間M到消息空間M的映射關(guān)系,。下面介紹網(wǎng)格環(huán)境下主要的函數(shù)關(guān)系,。(其中{x，y……}是一個集合,，＜x,，y＞是一個序偶^[6])。
　　S(Sid)：服務,。Sid服務標識,。
　　GS(GSid)：網(wǎng)格服務管理者，GSid網(wǎng)格服務標識,。
　　CCS(CCSid)：協(xié)同計算服務管理者,，CCSid協(xié)同計算標識。
　　CA(x)：頒發(fā)證書給x的認證中心,。
　　CCG(CCGid)：協(xié)同計算組,，由所有參與到該協(xié)同計算中的用戶組成, CCGid為協(xié)同計算標識,。
　　Sender(m)：某消息m的發(fā)送者集合。Sender(M)特指發(fā)送者集合,，該集合中的發(fā)送者均發(fā)送過消息,。
　　Accepter(m)：某消息m的接收者集合。Accepter(M)特指接收者集合,，該集合中的接收者均接收過消息,。
　　SenderAccepter(M)：笛卡爾集，笛卡爾集中每個元素都是一個序偶,。序偶中前一個元素為消息集M中任意消息的發(fā)送者,，后一個元素為該消息的接收者。
　　Req(S(Sid))：表示要求提供服務S(Sid)的請求,。
　　Requester(Req(S(Sid)))：服務請求Req(S(Sid))的發(fā)起者集合,。Requester(Req(S))特指服務請求發(fā)起者集合，該集合中的發(fā)起者均發(fā)起過服務請求,。
　　Responser(Req(S(Sid)))：服務請求Req(S(Sid))的響應者集合,。Responser(Req(S)特指服務請求響應者集合，該集合中的響應者均響應過服務請求,。
　　RequesterResponser(S)：笛卡爾集,，其中每個元素都是一個序偶。序偶中前一個元素為服務請求的發(fā)起者,，后一個元素為該服務請求的響應者,。
　　Kpb(x)：x的公鑰" title="公鑰">公鑰。
　　Kpv(x)：x的私鑰,。
　　Ses(＜x,，y＞)：x向y發(fā)送消息的會話密鑰，與Ses(＜y,，x＞)未必相同,。
　　E(m，k)：以密鑰k對消息m進行加密,。
　　D(m，k)：以密鑰k對消息m進行解密,。
　　S(m,，k)：以密鑰k對消息m進行簽名。
　　H(m,，k)：m的單向散列函數(shù),，k可有可無。
　　F(m1,，m2)：一般函數(shù),，用于密鑰的協(xié)商運算,。
　　Cert(CA(x)，x)：x在其認證中心CA(x)上注冊的公鑰證書,。證書由以下四部分組成：①主體名稱N(x),，用來明確認證證書所表示的人或其他對象；②屬于這個主體的公鑰Kpb(x),，用于X．509認證,；③簽署證書的認證中心標識ID(CA(x))，認證中心的身份標識,；④簽署證書的認證中心的數(shù)字簽名S(m,，Kpv(CA(x)))，用來確認認證中心的合法性,。
　　PCert(＜x,，y＞)：x給y頒發(fā)的代理證書，它也由以下四部分組成：①主體名稱N(y),，用來明確認證證書所表示的人或其他對象,；②屬于這個主體的公鑰Kpb(y)，用于X．509認證,；③簽署證書的主體x的標識ID(x),；④簽署證書的主體x的數(shù)字簽名S(m，Kpv(x)),，用來確認x的合法性,。
　　(4)動作：主體進行的活動。動作通常帶有各種參數(shù),，分別指明動作的發(fā)起者,、接收者、動作涉及的信息,、動作發(fā)起者本次協(xié)議的執(zhí)行標志,。R為協(xié)議的執(zhí)行標志。主要動作如下：
　?、賁end(＜x,，y＞，m,，R)：1表示發(fā)送者x發(fā)送消息m成功,；0表示發(fā)送者x發(fā)送消息m失敗。
　?、贏ccept(＜x,，y＞，m,，R)：1表示接收者x成功地收到來自于發(fā)送者y的消息m,；0表示接收者x未收到來自于發(fā)送者y的消息m,，接收失敗。
　?、跥enerate(x,，m1，m2,，R)：1表示主體x以消息m1為基礎(chǔ)成功地生成消息m2,；0表示主體x以消息m1為基礎(chǔ)生成消息m2失敗。
　?、蹹estroy(x,，m，R)：1表示主體x成功地在本地銷毀消息m,；0表示主體x在本地銷毀消息m失敗,。
　　⑤Execute(＜x,，y＞,，S(Sid)，R)：1表示主體x為主體y成功地提供某項服務S(Sid),；0表示主體x向主體y提供服務S(Sid)失敗,。
　　(5)謂詞：表示各種關(guān)系和狀態(tài)。主要有以下幾個謂詞：
　　Know(x,，m,，R)：1表示主體x知道消息m；0表示主體x不知道消息m,。當x是由多個用戶組成的組時,，表示組內(nèi)的所有用戶共享消息m。
　　Authen(＜x,，y＞,，m，R)：1表示主體x確認消息m為主體y所發(fā),，且發(fā)出后m未經(jīng)篡改,；0表示主體x確認m為主體x所發(fā)且消息m發(fā)出后未被篡改，二者不同時為真,，至少有一個為假,。　　
　　Author(＜x,，y＞，S(Sid),，R)：1表示主體x授權(quán)主體y享有獲得服務S(Sid)的權(quán)利,；0表示主體x未授權(quán)主體y享有獲得服務S(Sid)的權(quán)利,，即主體y無權(quán)享有主體x為其提供的服務S(Sid)。
　　Fresh(m,，R)：1表示消息m是新鮮的,，不是重用的；0表示消息m不是新鮮的,，是重用的,。
　　Compromise(m，R)：1表示消息m已經(jīng)泄露,；0表示消息m未被泄漏,。
　　Alter(m，R)：1表示消息m已經(jīng)被篡改,；0表示消息m未被篡改,。
　　Time_out(m，R)：1表示消息m已經(jīng)超過時間戳規(guī)定的有效期,，已作廢,；0表示消息m在時間戳規(guī)定的有效期內(nèi)，可以繼續(xù)使用,。
　　Group(＜CCG(CCGid),，x＞，R)：1表示主體x成為協(xié)同計算組CCG(CCGid)的成員,；0表示主體x不是協(xié)同計算組CCG(CCGid)的成員,。
　　安全需求可以描述成規(guī)則的形式。下面分析網(wǎng)格環(huán)境下某一多用戶協(xié)同計算問題的安全需求,，用以說明如何使用該語言,。
2 網(wǎng)格環(huán)境下多用戶協(xié)同計算問題的安全需求
　　網(wǎng)格是一種新型的分布式系統(tǒng)，它具有動態(tài)性,、多樣性,、自適應性等顯著特點。在網(wǎng)格環(huán)境下,，安全問題更加重要,。在網(wǎng)格計算中，最能體現(xiàn)網(wǎng)格計算的特點的是“多用戶參與的協(xié)同計算”,，同時它的安全需求最為復雜,。這種計算是指多個接入網(wǎng)格的用戶之間需要共同完成某項計算任務。
　　下面,，采用安全協(xié)議形式化需求語言描述網(wǎng)格環(huán)境下多用戶協(xié)同計算問題的安全需求,。在此舉例如下：某地區(qū)氣象部門計算該地區(qū)某時刻的氣象情況，該問題屬于網(wǎng)格環(huán)境下多用戶協(xié)同計算問題。分布在不同地點的用戶加入到協(xié)同計算組中,，利用各自采集的基礎(chǔ)數(shù)據(jù)作為輸入,，調(diào)用共同的計算過程。另外,，計算過程中可能會用到協(xié)同計算組之外的某些網(wǎng)格服務,。計算結(jié)束后，某些特定的參與者將獲得特定的計算結(jié)果,。
　　計算過程如下：N個參與者(N₁,，N₂，N₃……)加入到協(xié)同計算組中,，該協(xié)同計算過程由協(xié)同計算管理者管理,，該管理者將計算過程P分解為P₁，P₂,，P₃……,，并發(fā)送給N₁，N₂,，N₃……,。每個協(xié)同計算參與者N_i從其他參與者N_j處獲得數(shù)據(jù)集D_j來擴展自己的數(shù)據(jù)集，然后基于擴展后的數(shù)據(jù)集計算出結(jié)果MD_i,，并將結(jié)果MD_i發(fā)送給需要者Nk,。重復此過程，直到得到最終的結(jié)果集R_i,。最后,，將最終結(jié)果集R_i發(fā)送給特定的參與者N_i。其間,，會調(diào)用某些協(xié)同計算組之外的網(wǎng)格服務S_i,。
　　對于以上問題，為了簡化書寫,，特作如下定義：x表示主體,，該主體只有一個用戶；G代表所有參與到協(xié)同計算組的成員所組成的集合,；CCG為協(xié)同計算管理者,；s代表協(xié)同計算組中提供的某項服務，S代表協(xié)同計算組可以提供的全部服務,，K是所有密鑰的集合,，由公鑰集合KPB、私鑰KPC和會話密鑰SUS這三個集合中的所有元素構(gòu)成,；Cert為所有證書的集合,，由認證中心頒發(fā)的證書和代理證書組成,；R為動作發(fā)起者本次協(xié)議的執(zhí)行標志，R?代表某次協(xié)議的執(zhí)行標志,。
　　先給出非形式化描述,，再給出形式化描述。安全需求包括：
　　(1)認證
　　需求：協(xié)同計算組中的每個成員在成為協(xié)同計算組中的一員參與到該協(xié)同計算中之前,，都必須先將證書作為身份標識，提交給協(xié)同計算組,，通過協(xié)同計算組的身份驗證,。

　　經(jīng)過身份認證之后，協(xié)同計算組頒發(fā)給每位被認證的用戶一份代理證書PCert(GS,，x),，代理證書在協(xié)同計算過程中供用戶之間進行認證時使用。
　　需求：協(xié)同計算組要向每個組內(nèi)用戶發(fā)送一份代理證書,，每個組內(nèi)用戶也必須要收到一份來自于協(xié)同計算組的代理證書,。

　　(2)會話密鑰的保密性
　　需求：任何兩個相互通信的用戶之間共享通信密鑰，該密鑰不為第三者得知,。

　　(3)相互間的身份鑒別
　　需求：服務的提供方和請求方在進行服務之前要進行相互間的身份鑒別,，以確定對方的身份。

　　(4)授權(quán)和訪問控制
　　協(xié)同計算組中的成員有權(quán)參與協(xié)同計算,，但不是每個成員都有權(quán)享有協(xié)同計算中所提供的全部服務,，僅授權(quán)特定的成員享用特定的服務。用戶僅能享用他們被授權(quán)的服務,，不能使用他們未被授權(quán)的服務,。
　　需求：當且僅當獲得服務授權(quán)的用戶提出服務請求時，才會獲得服務,。

　　(5)通信保密性
　　需求：發(fā)送者與接收者共享會話密鑰,，發(fā)送者采用該密鑰發(fā)送消息，接收者能成功收到該消息,，并且該消息未被泄漏,。

　　(6)通信的完整性
　　需求1：發(fā)送者將消息m發(fā)送給接收者，在此過程中,，消息m未被篡改,。

　　需求2：所有用戶均可以成功地以消息m1為基礎(chǔ)生成新的消息m2。