关键词: DolevYao攻击者模型, 形式化描述, 模型检测, SPIN, NSPK, A(0)

Abstract:

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

Key words: DolevYao intruder model；formalization description；model checking；SPIN；NSPK；A(0)