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.