安全协议提供安全服务,是构建网络安全的基石。随着网络的迅速发展,越来越多的密码技术被应用到安全协议中,保证了网络不同程度的安全性。然而各种针对协议的攻击技术也不断出现,这对安全协议的分析提出了更高的要求。形式化方法是一种非常有效的安全协议分析的方法。串空间模型及相关理论的出现推动了安全协议的形式化分析研究。然而原始的串空间模型及其认证方法在分析一些安全协议时还存在一些不足,因此本文针对基于丰富密码学的安全协议和基于猜测攻击的安全协议,扩展了串空间模型和认证测试方法。由于原始的串空间模型仅考虑了一些简单操作,无法描述和分析在安全协议中使用越来越广泛的其他一些操作,如散列函数、签名运算和DH计算等,因此需要扩展串空间模型。由于认证测试方法以串空间模型为基础,因此串空间模型中存在的一些不足在认证测试方法中同样存在,因此本文还提出了一种基于丰富密码学的扩展认证测试方法。扩展后的模型和方法能够更精确地描述和分析安全协议的安全性,并能够应用于更广泛的领域。由于分析安全协议猜测攻击时需要考虑密码系统不完善所产生的问题,而原始的认证测试方法对密码系统做了完善的假设,需要三个基本前提假设,难以发现安全协议中存在的猜测攻击。本文提出了一种基于猜测攻击的扩展认证测试方法。首先定义了猜测数据和验证项,并将其引入到串空间模型中;然后定义了验证项判断规则和验证项判断算法,并将其引入到认证测试方法中。扩展后的模型和方法能够发现安全协议中存在的猜测攻击。为验证扩展串空间模型和认证测试方法的有效性,本文首先分析了SSL3.0和TLS1.0握手协议,验证了协议的认证性;然后分析了Yahalom-BAN和EXE协议,发现了协议中存在的猜测攻击。实例分析结果说明了扩展说明了扩展串空间模型和认证测试方法的正确性和有效性。