安全協(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)不適合于描述復(fù)雜的分布式系統(tǒng)，特別是網(wǎng)格系統(tǒng)。該語言一般適用于兩個用戶的系統(tǒng)，對于多用戶的復(fù)雜分布式系統(tǒng)，該語言的描述非常繁瑣，甚至無能為力。
　　(3)該語言還不夠嚴謹，有些定義是冗余的，有些定義是模糊的，不夠清晰。以上這些問題造成了該語言在實際應(yīng)用中的局限性，無法充分地發(fā)揮作用。本文在以上幾個方面作了改進，解決了以上幾個方面存在的不足，使該語言更加成熟。這種改進的安全協(xié)議的形式化需求語言主要是針對網(wǎng)格這一典型的復(fù)雜分布式系統(tǒng)的需求而設(shè)計的。將本語言簡化后，還可以適用于簡單的分布式系統(tǒng)。
1 改進的安全協(xié)議形式化需求語言
　　本語言由有限個常量項、變量項、n元函數(shù)、n元動作、原子謂詞公式、復(fù)合公式、邏輯連接符(包括∧、∨、┐、→、等)和時態(tài)操作符θ^[5]等組成。時態(tài)操作符θ表示某個動作發(fā)生在過去的某個時刻。
　　復(fù)雜的分布式系統(tǒng)存在用戶量大的特點，為了適應(yīng)這個特點引入了集合^[6]，用來表達組的概念，描述組內(nèi)的成員在某個方面具有某項共同的性質(zhì)和某種共同的行為。這樣可以使本語言更加簡潔。
　　(1)主體x：是一個有限集，集合中的元素是網(wǎng)格中的用戶，或者是用戶的代理。其中包括誠實用戶、攻擊者用戶和可信第三方(誠實的、能夠協(xié)助運算順利完成的第三方，例如網(wǎng)格服務(wù)管理者、協(xié)同計算服務(wù)管理者、證書認證中心等)及其代理?？占?覫代表集合中不含有用戶，全集E表示集合中含有全部用戶。最常見的主體是由一個用戶組成的集合。對主體的兩種運算(集合的并集、集合的減法，即組內(nèi)用戶數(shù)目的增多與減少)構(gòu)成了主體空間X：
　　x₁∪x₂∈X
　　x₁-x₂∈X
　　(2)消息m：是通信的內(nèi)容。有三種原子消息：主體標識、密鑰和新鮮數(shù)(包括隨機數(shù)和時間戳)。對原子消息和有效消息(有效信息是指通信中最終要傳輸?shù)?、包含有某些實際信息的消息，以上三種原子消息，最終都是為了傳輸有效消息服務(wù))的四種運算(合成、分解、加密和解密)構(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)：服務(wù)。Sid服務(wù)標識。
　　GS(GSid)：網(wǎng)格服務(wù)管理者，GSid網(wǎng)格服務(wù)標識。
　　CCS(CCSid)：協(xié)同計算服務(wù)管理者，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))：表示要求提供服務(wù)S(Sid)的請求。
　　Requester(Req(S(Sid)))：服務(wù)請求Req(S(Sid))的發(fā)起者集合。Requester(Req(S))特指服務(wù)請求發(fā)起者集合，該集合中的發(fā)起者均發(fā)起過服務(wù)請求。
　　Responser(Req(S(Sid)))：服務(wù)請求Req(S(Sid))的響應(yīng)者集合。Responser(Req(S)特指服務(wù)請求響應(yīng)者集合，該集合中的響應(yīng)者均響應(yīng)過服務(wù)請求。
　　RequesterResponser(S)：笛卡爾集，其中每個元素都是一個序偶。序偶中前一個元素為服務(wù)請求的發(fā)起者，后一個元素為該服務(wù)請求的響應(yīng)者。
　　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，接收失敗。
　　③Generate(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成功地提供某項服務(wù)S(Sid)；0表示主體x向主體y提供服務(wù)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ā)出后未被篡改，二者不同時為真，至少有一個為假?！　?BR>　　Author(＜x，y＞，S(Sid)，R)：1表示主體x授權(quán)主體y享有獲得服務(wù)S(Sid)的權(quán)利；0表示主體x未授權(quán)主體y享有獲得服務(wù)S(Sid)的權(quán)利，即主體y無權(quán)享有主體x為其提供的服務(wù)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)性、多樣性、自適應(yīng)性等顯著特點。在網(wǎng)格環(huán)境下，安全問題更加重要。在網(wǎng)格計算中，最能體現(xiàn)網(wǎng)格計算的特點的是“多用戶參與的協(xié)同計算”，同時它的安全需求最為復(fù)雜。這種計算是指多個接入網(wǎng)格的用戶之間需要共同完成某項計算任務(wù)。
　　下面，采用安全協(xié)議形式化需求語言描述網(wǎng)格環(huán)境下多用戶協(xié)同計算問題的安全需求。在此舉例如下：某地區(qū)氣象部門計算該地區(qū)某時刻的氣象情況，該問題屬于網(wǎng)格環(huán)境下多用戶協(xié)同計算問題。分布在不同地點的用戶加入到協(xié)同計算組中，利用各自采集的基礎(chǔ)數(shù)據(jù)作為輸入，調(diào)用共同的計算過程。另外，計算過程中可能會用到協(xié)同計算組之外的某些網(wǎng)格服務(wù)。計算結(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。重復(fù)此過程，直到得到最終的結(jié)果集R_i。最后，將最終結(jié)果集R_i發(fā)送給特定的參與者N_i。其間，會調(diào)用某些協(xié)同計算組之外的網(wǎng)格服務(wù)S_i。
　　對于以上問題，為了簡化書寫，特作如下定義：x表示主體，該主體只有一個用戶；G代表所有參與到協(xié)同計算組的成員所組成的集合；CCG為協(xié)同計算管理者；s代表協(xié)同計算組中提供的某項服務(wù)，S代表協(xié)同計算組可以提供的全部服務(wù)，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)相互間的身份鑒別
　　需求：服務(wù)的提供方和請求方在進行服務(wù)之前要進行相互間的身份鑒別，以確定對方的身份。

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

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

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

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