| 无线认证协议Linear MAKEP的模型检验 |
| |
| 引用本文： | 刘霞,陈维,彭军. 无线认证协议Linear MAKEP的模型检验[J]. 计算机工程, 2008, 34(3): 186-188 |
| |
| 作者姓名： | 刘霞 陈维 彭军 |
| |
| 作者单位： | 重庆科技学院电子信息工程学院,重庆,400050;重庆科技学院电子信息工程学院,重庆,400050;重庆科技学院电子信息工程学院,重庆,400050 |
| |
| 基金项目： | 重庆市自然科学基金 , 重庆市教委资助项目 |
| |
| 摘 要： | 模型检验是一种自动化程度很高的形式化分析技术。用有限状态机对无线认证协议Linear MAKEP建模，并对该协议的认证性用CTL公式进行形式化描述，将得到的模型和公式输入模型检验工具SMV进行检验。对检验结果进行分析发现：在Linear MAKEP协议中，入侵者可以冒充服务器与客户进行通信，不满足认证性。给出了协议的一种改进，使其满足认证性。
|
| 关 键 词： | LinearMAKEP协议 模型检验 认证性 形式化 |
| 文章编号： | 1000-3428（2008）03-0186-03 |
| 收稿时间： | 2007-02-10 |
| 修稿时间： | 2007-02-10 |
Model Checking of Wireless Authentication Protocol Linear MAKEP |
| |
| LIU Xia,CHEN Wei,PENG Jun. Model Checking of Wireless Authentication Protocol Linear MAKEP[J]. Computer Engineering, 2008, 34(3): 186-188 |
| |
| Authors: | LIU Xia CHEN Wei PENG Jun |
| |
| Affiliation: | (Electronic Information Engineering Institute, Chongqing University of Science and Technology, Chongqing 400050) |
| |
| Abstract: | Model checking is a formal analysis technique with high automation. Wireless authentication protocol Linear MAKEP is modeled by finite automatas and authentication of the protocol is formally specified with CTL formula. The obtained model and formula are verified by a model checking tool SMV. The result shows that in Linear MAKEP, an intruder can impersonate the server to communicate with the client, thus, the protocol can not guarantee authentication. An improvement is given, making the protocol guarantee authentication. |
| |
| Keywords: | Linear MAKEP protocol model checking authentication formalization |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载免费的PDF全文 |
