摘要：模型检测技术能够实现安全协议的自动化分析，是一种高效的形式化分析方法。然而，对于攻击者的建模却一直缺乏通用的方法，这导致了模型检测方法的自动化程度降低。本文为安全协议分析中，应用最为广泛的Dolev-Yao攻击者模型建立了一套形式化描述方法。遵循这一方法，可以使用任何建模语言机械地建立Dolev-Yao攻击者模型，从而大大地减少了人工分析的成份。同时，本文还使用该方法验证了两个目的完全不同的协议，证明了它的通用性。

关键词：形式化描述 模型检测 spin nspk 

单位：贵州大学计算机软件与理论研究所 贵州贵阳550025