该文中,我们探讨了形式化方法在安全协议验证领域内的相关应用问题.其中,我们工作的重点将集中在Strand空间方法上.首先,我们介绍了安全协议描述方法发展的三个阶段,由此引出形式化方法应用于安全协议验证领域内的初衷.随后,我们分三条线索:Dolev-Yao模型及其影响、BAN逻辑与其后续工作,以及形式化方法的自动化技术,对形式化方法在安全协议验证领域内的发展动态进行了全面而客观的评述.第二,我们概述了该领域内三个最具影响力的形式化方法的应用过程,它们分别是Dolev-Yao模型、BAN逻辑,与Strand空间.为了进一步说明这些方法的实用性,我们还给出了相应的实例分析.第三,我们对近来颇受关注的Strand空间展开了一系列研究.这部分工作基于五个目标:其一、细化理想结构的描述方式;基二、形式化表述安全密钥的概念;其三、揭示安全密钥与协议秘密属性之间的关系;其四、给出安全密钥的相关性质;其五、提出一个证明安全协议的新思路.为实现这些目标,我们引入新的记号以表示理想的内部结构;利用理想的概念给出了安全密钥的形式化描述;在特定条件下,通过对比安全密钥与秘密属性各自的理想表达,证明了他们之间的等价关系;借助入侵者密钥的定义与入侵者行为对应的消息序列,证明了安全密钥特有的性质;最后,基于以上工作,我们提出一个基于安全密钥概念的协议证明思路.第四,我们基于Strand空间提出了一个新的针对安全协议缺陷的分类法.这个分类法将协议缺陷分为以下八类:当前性缺失缺陷、方向性缺失缺陷、类型缺失缺陷、独立性缺失缺陷、轮数标识缺失缺陷、认证过程缺失缺陷、认证测试形式相同缺陷,与认证测试部分形式相同缺陷.并且,对于前四类协议缺陷,我们利用认证测试方法完成了相应的协议分析工作.最后,我们介绍了形式化方法在安全协议设计领域内的应用现状,并且讨论了这个领域内今后的研究方向.