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

Model Checking can verify security protocols automatically.It is an efficient formal method. But there lacks a general method to build the intruder model.It leads to the decrease of the automation degree of model checking. This paper gives a formalization description method of the DolevYao intruder model wich is most widely used in security protocols analysis.According to this method, we can use an arbitrary modeling language to build the DolevYao intruder model by rote.It greatly decreases the components of artificial analysis. Meanwhile,we use this method to verify two security protocols with different goals.It proves that our method is generalpurpose.