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.

Key words: Linear MAKEP protocol, model checking, authentication, formalization

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

关键词: Linear MAKEP协议, 模型检验, 认证性, 形式化

CLC Number: 

• TP311