Athena方法是安全协议分析领域中的一种新的形式化分析方法。本文首先对其进行了深入分析,然后针对安全协议形式化分析领域中的两个重要问题——类型缺陷攻击问题、组合协议猜测攻击问题及Athena方法在分析这两个问题中遇到的困难,对该方法进行了扩展。取得的主要成果如下:(1)对Athena方法进行了深入研究,分析了Athena方法对串空间模型所做的扩展,对Athena方法的逻辑和验证算法进行了深入分析,并通过实验说明其分析协议的有效性和高效性。(2) Athena方法建立在强类型抽象假设的基础上,但在协议的实际执行过程中,这样的假设并不现实。因此本文去除这一假设,对原有的Athena方法进行了相应的扩展,引入了组合项,增加了攻击者强制类型转换的能力,同时扩展了Athena方法中的内在项、目标及目标绑定等概念,并对相关内容进行修改。用扩展后的方法对NSL协议进行分析,发现了一处在APV中无法发现的类型缺陷攻击。(3)针对组合协议猜测攻击问题,对Athena方法进行扩展。引入了串空间模型中理想的概念,并在此基础上提出了一种跨协议影响的关系,以描述从协议对主协议的影响,增加了攻击者猜测密钥的能力,提出了猜测验证目标及猜测验证绑定的概念,对Athena方法中的状态、推理规则、后继状态函数等进行了扩展。用扩展后的Athena方法对一个认证协议实例和EKE协议的组合运行问题进行了分析,发现了认证协议实例在组合协议环境下存在的一处猜测攻击。