安全协议在信息安全中起着至关重要的作用。在实际应用中,人们需要可信的机制来为通信实体进行身份认证和分发密钥。然而,已有的安全协议往往被证实并不如它们的设计者所期望的那样安全,复杂的网络环境使得攻击者可利用安全协议设计中的缺陷和漏洞来实施各种各样的攻击,安全协议自身的安全性成了网络安全的关键问题之一。关于安全协议的研究主要包括两方面内容:安全协议的安全性分析方法研究和各种实用安全协议的设计与分析研究。安全协议的设计与分析是十分复杂的,大量的实例说明,即使设计一个参与主体与消息交换都很少的协议,确保其没有安全缺陷也是很困难的。因此,采用形式化的方法进行安全认证协议的设计,使用形式化分析方法对协议进行严谨的形式化分析是十分必要的。目前,有关安全协议研究的重点主要集中在形式化分析上,现在已取得不少成果。典型的形式化分析方法主要有三类:基于知识或信任的模态逻辑方法、基于模型检测的分析方法和基于定理证明的分析方法。安全协议形式化分析的研究也推动了安全协议设计的发展,然而,虽然目前已经有一些安全协议设计的理论与方法,但易于操作的实用方法和工具尚不多见。本文重点从三个方面对安全协议进行了研究:其一是提出了一种形式化设计安全认证协议的新方案PCDS,建立了模型并提出具体实现方法;其二是使用形式化的方法和自动化测试工具对设计的安全协议进行了分析;其三是通过扩展SIP协议,提出了一种用于视频会议快速安全认证的一种新协议APVC和安全方案。在安全协议设计方面,本文总结各种设计理论与方法,借鉴datta等人的思想提出了一种形式化设计安全认证协议的新方案。该方案建立了PCDS协议组合设计模型,提出了安全认证协议的生成理论,说明了该系统的使用方法,并用多个实例表明了这个系统的实用性。该方案主要基于Diffie-Hellman算法,把安全协议的设计按安全目标分成三层:第一层为基本的密钥交换与身份认证属性的实现;第二层为有关效率的提升与预防拒绝服务攻击的实现机制;第三层为安全协议安全属性的形式化分析与自动化测试。本系统可实现安全认证协议的形式化设计,可针对不同的环境和需求产生众多备选协议,并可对协议的安全性给予验证,还能根据需要方便地予以扩充和移植。使用这种方法可对现在实用的认证协议如IKE等进行推导设计。在安全协议的形式化分析方面,本文主要研究了PCL协议组合逻辑。PCL是用于证明网络协议安全属性的一种逻辑推导系统,PCL具有“相信逻辑”—BAN逻辑的易读性,同时具有Paulson等基于参与者和入侵者模型的归纳法PIM的相同安全证明等级。利用PCL可以证明安全协议的认证性和私密性等属性。本文使用PCL证明了两个本系统所设计的安全协议的认证属性和私密属性。在安全协议自动化测试方面,本文主要研究分析了HLPSL高级协议格式语言和AVISPA测试工具。并用AVISPA测试了一些备选协议实例,得出了有意义的测试结果。最后,研究了现有的视频会议系统中的常用身份认证方法,分析了其安全性和不足之处,针对安全性和效率问题,在SIP协议基础上做了具体的扩充方案,提出了一种用于视频会议快速安全认证的一种新协议APVC,并分析了该协议的安全性和效率,通过PCL和AVISPA工具证明,在D-Y模型下,该协议既具有基于证书的公钥密码体制的安全性,又具有效率的优势。