基于状态模型的四次握手协议验证

Verification of 4-Way Handshake Protocol Based on State Model

利用外部和内部事件状态模型方法抽象出四次握手协议的逻辑过程,并建立协议中重要性质的形式化模型(例如:消息发送顺序、分配密钥等)。Spin工具的特性是对状态模型和性质进行模型检测,通过对模型进一步检测和验证结果的分析,得出四次握手协议在密钥GTK分配上具有一定缺陷,并会导致GTK传送失败。

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.