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

Model Checking of Wireless Authentication Protocol Linear MAKEP

作　　者：刘霞[1] 陈维[1] 彭军[1] 

机构地区：[1]重庆科技学院电子信息工程学院,重庆400050

出　　处：《计算机工程》2008年第3期186-188,212,共4页Computer Engineering

基　　金：重庆市科委自然科学基金资助项目(CSTC;2005BB2050);重庆市教委科学技术研究基金资助项目(KJ051402)

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

关 键 词：LINEAR MAKEP协议 模型检验 认证性 形式化 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]