Formal Verification of IEEE802.11i Protocol Using Distributed Temporal Logic Formalization
Yong Zhou · Journal of Nantong University · 2010
On the basis of the distributed temporal logic introduced by Caleiro,we improve the Caleiro′s network model by adding the challenge-question set and the challenge-answer set.We convert IEEE802.11i protocol into the event-structure semantic model of the distributed temporal logic and formally prove the secrecy property of the protocol.The mutual authentication properties between the peer,authenticator and the radius server are also verified.The result of the analysis indicates the correctness of the IEEE802.11i protocol.