安全协议是建立在密码学基础上的网络协议,用于确保网络通信的安全可靠。近年来,随着网络需求的不断增长,安全协议的设计研究也逐步成为热点。但由于网络环境的复杂性,协议的安全性质往往难以保证,非形式化设计容易出错,因此人们寻求更为严格的形式化设计方法。　　本文主要研究了安全协议的形式化设计方法及其应用,包括BSW逻辑、协议自动生成APG、认证测试方法及组合设计方法等,所取得的主要研究成果有:　　(1)针对 BSW逻辑在公钥认证协议设计中的不足,消除了原合成规则对公钥使用者身份的不合理限制,指出了BSW逻辑忽略冗余性处理所带来的加密冗余问题;　　(2)对协议自动生成APG进行了系统的分析,设计生成了对称密钥体制下比原版本更加简单的两方互相认证协议,比较了APG相对于层次化设计方法的优势,分析了APG存在不足的原因并讨论了今后的研究方向;　　(3)在认证测试方法的基础上,引入了关键分量的概念,提出了多重认证测试方法;使用该方法重新设计了Woo-Lam单向认证协议;设计出的协议不仅避免了原协议经认证测试方法改进后存在的缺少主体标识的缺陷,而且避免了Abadi和Buttyan等人分别对原协议改进后存在的两个重放攻击;　　(4)使用组合设计方法,分别推导出了公钥体制下双向认证且交换秘密的协议框架和对称密钥体制下带有认证服务器的密钥分发协议框架,通过比较,指出了Needham-Schroeder认证协议存在的安全缺陷;归纳得到了分别针对银行、商家和客户的11条安全需求,重新设计了彭勋等人提出的SEP协议,分析表明,新协议满足指定的安全需求,实现了电子商品和实物商品在线支付的设计目标,满足匿名性、隐私性和可追究性,并适用于多个客户和商家对同时交易的情况。