10.3969/j.issn.1000-3428.2008.03.065
无线认证协议Linear MAKEP的模型检验
模型检验是一种自动化程度很高的形式化分析技术.用有限状态机对无线认证协议Linear MAKEP建模,并对该协议的认证性用CTL公式进行形式化描述,将得到的模型和公式输入模型检验工具SMV进行检验.对检验结果进行分析发现:在Linear MAKEP协议中,入侵者可以冒充服务器与客户进行通信,不满足认证性.给出了协议的一种改进,使其满足认证性.
LinearMAKEP协议、模型检验、认证性、形式化
34
TP311(计算技术、计算机技术)
重庆市自然科学基金CSTC2005BB2050;重庆市教委资助项目KJ051402
2008-04-15(万方平台首次上网日期,不代表论文的发表时间)
共4页
186-188,212