| Kerberos协议的形式分析与NuSMV检验 |
| |
| 引用本文： | 张春永.Kerberos协议的形式分析与NuSMV检验[J].盐城工学院学报(自然科学版),2009,22(4):39-43. |
| |
| 作者姓名： | 张春永 |
| |
| 作者单位： | 盐城工学院,信息工程学院,江苏,盐城,224051 |
| |
| 摘 要： | NuSMV是一个基于计算树逻辑的符号化模型检验工具。对Kerberos认证协议进行分析,并对其建立有限状态机模型,利用NuSMV保密性、认证性和活性等从3个方面进行了验证,指出Kerberos协议存在不安全性。
|
| 关 键 词： | 符号模型检测 计算树逻辑CTL NuSMV Kerberos协议 |
Form Analysis of Kerberos Protocal and NuSMV Verification |
| |
| ZHANG Chun-yong.Form Analysis of Kerberos Protocal and NuSMV Verification[J].Journal of Yancheng Institute of Technology(Natural Science Edition),2009,22(4):39-43. |
| |
| Authors: | ZHANG Chun-yong |
| |
| Institution: | ZHANG Chun-yong (School of Information Engineering, Yancheng Institute of Technology,Jiangsu Yancheng 224051, China) |
| |
| Abstract: | NuSMV is a symbolic model verification tool based on computation tree logic.The Kerberos authentication protocal was analysed,and the finite state model was set up.The non-security of Kerberos protocol exists which was verifing from security property,authentication and liveness using NuSMV. |
| |
| Keywords: | NuSMV |
| 本文献已被 维普 万方数据 等数据库收录！ |
| 点击此处可从《盐城工学院学报(自然科学版)》浏览原始摘要信息 |
| 点击此处可从《盐城工学院学报(自然科学版)》下载免费的PDF全文 |
