网格是一个集成的计算资源环境,其通过标准的、开放的、通用的协议和接口实现分布式资源的协同使用,并且,其能够向用户提供非平凡的服务质量。其中,网格环境下多用户参与的协同计算是网格的一个重要应用方向。与此同时,网格应用的发展对于运行的可靠性提出了更高的要求,而安全协议则是保证安全性的重要手段。在网格环境下,安全协议运行过程中实体之间的通讯主要通过虚拟组织来实现,即用户必须通过相关认证与授权加入虚拟组织来实现与虚拟组织其它成员之间进行通讯。由于网格虚拟组织具有层次化的管理结构,网格虚拟组织中的安全协议可能与其它安全协议之间存在并行运行。因此,尽管多数安全协议本身能够满足安全目标,非诚实实体仍然可能会对安全协议实施并行攻击。本文在网格虚拟组织的基础上对安全协议的形式化分析与验证进行了深入研究,主要研究内容包括：安全需求形式化描述,安全协议分析与验证,攻击反例自动化构造以及攻击消除。所完成的工作主要有：本文通过在传统串空间模型的基础上引入网格计算代理的概念,把安全协议参与者与虚拟组织中网格计算代理联系起来,提出了一种新的网格虚拟组织环境下安全协议的形式化分析与验证方法,以及一种基于网格虚拟组织的安全协议形式化拆分方法。并且,本文在此基础上进一步提出了一种在网格虚拟组织环境下制定和部署二级动态授权策略的方法,其通过限制协议参与者在拆分后子协议之间可能存在的协同行为,最终实现消除网格虚拟组织环境下安全协议非诚实参与者的并行攻击。本文同时利用所提出安全协议形式化拆分方法成功消除了网格虚拟组织环境下一种针对Diffie-Hellman双向认证协议的并行攻击。Athena安全协议自动化验证工具基于传统的串空间模型实现了对安全协议的自动化验证。由于传统的串空间模型无法对从属于同一代理的不同串之间的信息共享进行定义,Athena安全协议自动化验证工具不能完整构造网格虚拟组织环境下安全协议非诚实参与者的并行攻击反例。本文通过在传统串空间模型的基础上引入网格计算代理的概念,对Athena安全协议自动化验证工具中的安全属性定义以及安全证据推导过程进行了扩展,使得新的逻辑系统能够支持多代理系统,这样在很大程度上减少了原有系统中存在的状态爆炸现象。在此基础上,本文提出了一种新的网格虚拟组织环境下安全协议攻击反例的自动化构造方法。本文同时利用所提出自动化方法构造出网格虚拟组织环境下针对Diffie-Hellman双向认证协议的攻击反例。当前安全协议形式分析技术面对的主要挑战之一是如何对复杂密码操作进行形式化定义。传统的安全协议分析技术只对包括加密和数字签名在内的基本密码操作进行了形式化定义,此类基本密码操作仅仅具备认证性与秘密性的安全属性。而现代安全协议中则出现了许多新的密码操作,此类密码操作具备了比基本密码操作更为复杂的安全属性。秘密共享就属于这样一类密码操作。本文基于等值理论在应用Pi演算中对可验证的多秘密共享方案的密码学语义进行了形式化定义。在此基础上,本文进一步提出了一种用于将所提出有限等值理论转化为安全协议自动化验证器Proverif中重写机制的编码方法,并且,最终在Proverif中实现了关于可验证的多秘密共享方案的形式化验证。本文同时利用所提出有限等值理论在Proverif中对门限证书协议进行了验证。