无线认证协议Linear MAKEP的模型检验

• 作者: 刘霞 彭军 陈维
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: LinearMAKEP协议 模型检验 认证性 形式化
• 年，卷（期）: 2008,（3）
• 所属期刊栏目: 安全技术
• 页码范围: 186-188,212
• 页数: 4页
• 分类号: TP311
• 字数: 3104字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2008.03.065

摘要

模型检验是一种自动化程度很高的形式化分析技术.用有限状态机对无线认证协议Linear MAKEP建模,并对该协议的认证性用CTL公式进行形式化描述,将得到的模型和公式输入模型检验工具SMV进行检验.对检验结果进行分析发现:在Linear MAKEP协议中,入侵者可以冒充服务器与客户进行通信,不满足认证性.给出了协议的一种改进,使其满足认证性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	彭军	重庆科技学院电子信息工程学院	38	329	8.0	17.0
2	刘霞	重庆科技学院电子信息工程学院	2	9	1.0	2.0
3	陈维	重庆科技学院电子信息工程学院	2	8	1.0	2.0