基于模型检测的NS公钥认证协议分析  

Analysis of Needham-Schroeder Symmetric Key Authentication Protocol Based on Model Checking

作　　者：刘玉坤[1] 张浩军[1] 

机构地区：[1]河南工业大学信息科学与工程学院计算机工程系,郑州450001

出　　处：《计算机与数字工程》2009年第2期90-93,101,共5页Computer & Digital Engineering

摘　　要：模型检测的研究大致包括以下内容:模态逻辑、模型检测算法及其空间效率的改进。以NS认证协议的模型形式化与分析为例,对模型检测的思想进行说明,并利用惰性语言Haskell实现了上述模型形式化与分析,并成功找到了中间人攻击序列。Research on model checking covers the following subjects： modal/temporal logics, model checking algorithms, efficiency of model checking. This paper presents these ideas of model checking with the analysis of Needham- Schroeder symmetric key authentication protocol, and realize it use lazy evaluation, programming language- Haskell, which successfully find the Man- in- the - Middle Attack.

关 键 词：安全协议 形式化分析 模型检测 HASKELL 

分 类 号：TN918.1[电子电信—通信与信息系统]