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

• 作者: 唐郑熠 李祥
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: Dolev-Yao攻击者模型 形式化描述 模型检测 SPIN NSPK A(0)
• 年，卷（期）: 2010,（8）
• 页码范围: 36-38,45
• 分类号: TP393.08
• 字数: 3865字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2010.08.010

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李祥	贵州大学计算机软件与理论研究所	91	551	13.0	19.0
2	唐郑熠	贵州大学计算机软件与理论研究所	12	63	4.0	7.0