Dolev-Yao攻击者模型的形式化描述 |
| |
引用本文: | 唐郑熠,李祥.Dolev-Yao攻击者模型的形式化描述[J].计算机工程与科学,2010,32(8). |
| |
作者姓名: | 唐郑熠 李祥 |
| |
作者单位: | 贵州大学计算机软件与理论研究所,贵州,贵阳,550025 |
| |
摘 要: | 模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的Dolev-Yao攻击者模型建立了一套形式化描述方法。遵循这一方法,可以使用任何建模语言机械地建立Dolev-Yao攻击者模型,从而大大地减少了人工分析的成份。同时,本文还使用该方法验证了两个目的完全不同的协议,证明了它的通用性。
|
关 键 词: | Dolev-Yao攻击者模型 形式化描述 模型检测 SPIN NSPK A(0) |
本文献已被 万方数据 等数据库收录! |
|