无线网协议802.11i安全性的一种形式化分析方法  

Security analysis of 802.11i based on Strand Spaces

作　　者：张招亮[1] 张广泉[1] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006

出　　处：《苏州大学学报（自然科学版）》2008年第3期39-44,共6页Journal of Soochow University(Natural Science Edition)

基　　金：江苏省高校自然科学研究项目(05KJB520119);重庆市自然科学基金资助项目(CSTC;2006BB2259)

摘　　要：首先建立了无线环境中入侵者的能力模型,再应用串空间模型形式化地分析了802.11i的四次握手协议的保密特性.分析结果表明,在提出的模型下,四次握手协议能安全地分配PTK和GTK.It has been proved that the 802.11 protocol may encounter a number of threats such as message authentication and integrity, key sequence reuse and key distribution and management. As a remedy, IEEE has designed 802. 11 i to address these security issues. We aim to analyze the seurity property of 802.11 i. We introduce the capacity model of the penetrator in wireless environment, then analyze security property of the 4-way handshake protocol of 802.1 1i. Our analysis proves that 4-way handshake can distribute PTK and GTK safely under the presented model.

关 键 词：无线网 802.11i 安全性 串空间 形式化分析 

分 类 号：TP919.2[自动化与计算机技术]