Dolev-Yao攻击者模型的形式化描述

The Formalization Description of the Dolev-Yao Intruder Model

模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的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 thc 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.