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

Model Checking of Wireless Authentication Protocol Linear MAKEP

模型检验是一种自动化程度很高的形式化分析技术。用有限状态机对无线认证协议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.