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

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

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

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

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

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

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

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