Model Checking of Wireless Authentication Protocol Linear MAKEP
Jun Peng · Jisuanji gongcheng · 2008
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.