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

摘要：

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

关键词：Dolev-Yao攻击者模型、形式化描述、模型检测、SPIN、NSPK、A(0)

所属期刊栏目：32

分类号：TP393.08(计算技术、计算机技术)

在线出版日期：2010-11-03（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：36-38,45