Verification of 4-Way Handshake Protocol Based on State Model
Xiu Jin · Modern Computer · 2009
By carefully studying the interior and exterior state of the model, aims to abstract and analyze the complicated logical process of the 4-way handshake system and summarize some important characters such as sequence of message sending, key assigning so on so forth. Tests the state and quality of the model with the help of the characters of Spin and analyzes the results. Finally it is found that some bugs in the process of assigning GTK would result in failed sending.