Analysis and Improvement of Formal Security Models of Three-Party Authentication and Key Distribution Protocol
In this paper, the authors analyze the formal security models of three party authentication and key distribution protocol, which are Extended BR and Extended CK model. They propose the flaw about definition of session identifier in the Extended CK model and present the limitation in the definition of matching conversation for Extended BR model. According to the rules of 802.11i standard, a new formal security model of three-party authentication and key distribution protocol was defined by \"Efficient AP\", and they present a provable secure EAP-TLS protocol in their model. The new formal security model provides a better method for resolving the security problems of three-party authentication and key distribution protocol in WLAN.