Kerberos协议的形式分析与NuSMV检验

• 作者: 张春永
• 来源期刊: 盐城工学院学报（自然科学版）
• 学科: 工学
• 关键词: 符号模型检测 计算树逻辑CTL NuSMV Kerberos协议
• 年，卷（期）: 2009,（4）
• 所属期刊栏目: 计算机应用研究
• 页码范围: 39-43
• 页数: 5页
• 分类号: TP39
• 字数: 4094字
• 语种: 中文
• DOI: 10.3969/j.issn.1671-5322.2009.04.012

摘要

NuSMV是一个基于计算树逻辑的符号化模型检验工具.对Kerberos认证协议进行分析,并对其建立有限状态机模型,利用NuSMV保密性、认证性和活性等从3个方面进行了验证,指出Kerberos协议存在不安全性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张春永	盐城工学院信息工程学院	2	0	0.0	0.0