安全协议是用来实施安全功能的一种重要的安全技术，是许多分布式系统安全的基础。设计一种正确的、符合安全目标、没有冗余的安全协议，是一件非常困难的事情。为此，人们越来越多地关注形式化方法，期望建立一套完整成熟的理论和技术，并将该理论和技术用于实践中，设计、验证和改进安全协议。
　　安全协议设计和分析的困难性是由多方面因素造成的。其中最先遇到的问题就是安全问题本身的微妙性^[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为协议的执行标志。主要动作如下：
　　①Send(＜x，y＞，m，R)：1表示发送者x发送消息m成功；0表示发送者x发送消息m失败。
　　②Accept(＜x，y＞，m，R)：1表示接收者x成功地收到来自于发送者y的消息m；0表示接收者x未收到来自于发送者y的消息m，接收失败。
　　③Generate(x，m1，m2，R)：1表示主体x以消息m1为基础成功地生成消息m2；0表示主体x以消息m1为基础生成消息m2失败。
　　④Destroy(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)谓词：表示各种关系和状态。主要有以下几个谓词：
　　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发出后未被篡改，二者不同时为真，至少有一个为假。　　
　　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。