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

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

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

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

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

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

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

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