第３２卷第９期２０１０年９月电子与信息学报ＪｏｕｒｎａｌｏｆＥｌｅｃｔｒｏｎｉｃｓ＆ＩｎｆｏｒｍａｔｉｏｎＴｅｃｈｎｏｌｏｇｙＶｂＩ．３２Ｎｏ．９Ｓｅｐｔ．２０１０协议组合逻辑安全的ＷｉＭＡＸ无线网络认证协议冯涛①＠＠张子彬①马建峰＠①（兰州理工大学计算机与通信学院兰州７３００５０）⑦（西安电子科技大学计算机网络与信息安全教育部重点实验室西安７１００７１）＠（福建师范大学网络安全与密码技术重点实验室福州３５０００７）摘要：国际标准ＩＥＥＥ８０２．１６ｅ－２００５中ＰＫＭ、ｒ２协议的安全性是ＷｉＭＡＸ无线网络安全的重要保证。论文基于协议组合逻辑（ＰＣＬ）分析了ＰＫＭｖ２协议中认证协议的安全性，发现ＰＫＭｖ２安全认证协议存在交错攻击，在此基础上基于协议演绎系统（ＰＤＳ）提出了一种新的ＷｉＭＡＸ无线网络安全认证协议，并使用协议组合逻辑（ＰＣＬ）给出新协议的模块化正确性和安全性证明，新协议相对于ＰＫＭｖ２安全认证协议更加安全，更适应ＷｉＭＡＸ无线网络复杂的网络应用环境。关键词：无线网络；认证协议；协议演绎系统；协议组合逻辑；ＷｉＭＡＸ中图分类号：ＴＰ３０９文献标识码：Ａ文章编号：１００９－５８９６（２０１０）０９－２１０６－０６ＤＯＩ：１０．３７２４／ＳＰ．Ｊ．１１４６．２００９．０１１９１ＳｅｃｕｒｉｔｙＡｕｔｈｅｎｔｉｃａｔｉｏｎＰｒｏｔｏｃｏｌｆｏｒＷｉＭＡＸＷｉｒｅｌｅｓｓＮｅｔｗｏｒｋＢａｓｅｄｏｎＰｒｏｔｏｃｏｌＣｏｍｐｏｓｉｔｉｏｎＬｏｇｉｃＦｅｎｇＴａｏ∞固ＺｈａｎｇＺｉ—ｂｉｎ①ＭａＪｉａｎ－ｆｅｎｇ《Ｄ…（Ｓｃｈｏｏｌｏ／ＣｏｍｐｕｔｅｒａｎｄＣｏｍｍｕｎｉｃａｔｉｏｎ，ＬａｎｚｈｏｕＵｎｉｖｅｒｓｉｔｙＤ，Ｔｅｃｈｎｏｌｏｇｙ，Ｌａｎｚｈｏｕ７３００５０，Ｃｈｉｎａ）’（ＫｅｙＬａｂｏｒａｔｏｒｙｏ｛ＣｏｍｐｕｔｅｒＮｅｔｗｏｒｋｓａｎｄＩｎｆｏｒｍａｔｉｏｎＳｅｃｕｒｉｔｙｏｌＭｉｎｉｓｔｒｙｏ／ＥｄｕｃａｔｉｏｎＩＸｉｄｉａｎＵｎｉｖｅｒｓｉｔｙ，Ｘｉ’ａｎ７１００７１，Ｃｈｉｎａ）…（ＫｅｙＬａｂ吖ｔｈｅＮｅｔｗｏｒｋＳｅｃｕｒｉｔｙａｎｄＣｒｙｐｔｏｌｏｇｙ，ＦｕｊｉａｎＮｏｒｍａｌＵｎｉｖｅｒｓｉｔｙ，Ｆｕｚｈｏｕ３５０００７，Ｃｈｉｎａ）Ａｂｓｔｒａｃｔ：ＩＥＥＥ８０２．１６ｅ－２００５ｓｔａｎｄａｒｄ’ＳＰＫＭｖ２ｐｒｏｔｏｃｏｌｉｓ衄ｉｍｐｏｒｔａｎｔｓｅｃｕｒｅｇｕａｒａｎｔｅｅｆｏｒＷｉＭＡＸ（ＷｏｒｌｄｗｉｄｅＩｎｔｅｒｏｐｅｒａｂｉｌｉｔｙｆｏｒＭｉｃｒｏｗａｖｅＡｃｃｅｓｓ）ｗｉｒｅｌｅｓｓｎｅｔｗｏｒｋ．Ｉｎｔｈｉｓｐａｐｅｒ，ｂａｓｅｄｏｎＰｒｏｔｏｃｏｌＣｏｍｐｏｓｉｔｉｏｎＬｏｇｉｃ（ＰＣＬ），ｔｈｅＰＫＭｖ２ａｕｔｈｅｎｔｉｃａｔｉｏｎｐｒｏｔｏｃｏｌ’Ｓｓｅｃｕｒｉｔｙｉｓａｎａｌｙｚｅｄ，ｔｈｅｉｎｔｅｒｌｅａｖｉｎｇａｔｔａｃｋｉｓｆｏｕｎｄ，ａｎｄａｎｅｗａｕｔｈｅｎｔｉｃａｔｉｏｎｐｒｏｔｏｃｏｌｉｓｐｒｏｐｏｓｅｄｂｙｕｓｉｎｇｔｈｅＰｒｏｔｏｃｏｌＤｅｒｉｖａｔｉｏｎＳｙｓｔｅｍ（ＰＤＳ）ｉｎＷｉＭＡＸｗｉｒｅｌｅｓｓｎｅｔｗｏｒｋｂａｓｅｄｏｎｔｈｅｖｕｌｎｅｒａｂｉｌｉｔｙｏｆｓｙｓｔｅｍｓｅｃｕｒｉｔｙｆｉｎａｌｌｙａｆｏｒｍａｌｃｏｒｒｅｃｔｎｅｓｓａｎｄｓｅｃｕｒｉｔｙｐｒｏｏｆｏｆｉｔｉｓｐｒｅｓｅｎｔｅｄｗｉｔｈＰｒｏｔｏｃｏｌＣｏｍｐｏｓｉｔｉｏｎＬｏｇｉｃ（ＰＣＬ）．ＴｈｉｓｎｅｗｐｒｏｔｏｃｏｌｉｓｍｏｒｅｓｅｃｕｒｅｔｈａｎｔｈｅＰＫＭｖ２ｓｅｃｕｒｉｔｙａｕｔｈｅｎｔｉｃａｔｉｏｎｐｒｏｔｏｃｏｌ，ａｎｄｍｏｒｅｓｕｉｔａｂｌｅｆｏｒｃｏｍｐｌｉｃａｔｅｄｗｉｒｅｌｅｓｓｎｅｔｗｏｒｋａｐｐｌｉｃａｔｉｏｎｅｎｖｉｒｏｎｍｅｎｔｕｓｅｄｉｎＷｉＭＡＸ．Ｋｅｙｗｏｒｄｓ：Ｗｉｒｅｌｅｓｓｎｅｔｗｏｒｋ；Ａｕｔｈｅｎｔｉｃａｔｉｏｎｐｒｏｔｏｃｏｌ；ＰｒｏｔｏｃｏｌＤｅｒｉｖａｔｉｏｎＳｙｓｔｅｍ（ＰＤＳ）；ＰｒｏｔｏｃｏｌＣｏｍｐｏｓｉｔｉｏｎＬｏｇｉｃ（ＰＣＬ）；ＷｉＭＡＸ１引言宽带无线接入技术是指以无线传输方式向用户提供接入宽带固定网络的接入技术。２００５年ＩＥＥＥ８０２．１６－Ｅ作组推出了ＷｉＭＡＸ无线网络的国际新标准ＩＥＥＥ８０２．１６ｅ－２００５１１－３Ｊ，ＷｉＭＡＸ（全球微波接入２００９－０９－０８收到，２０１０－０２－０９改回国家高技术研究发展计划（８６３）（２００７ＡＡ０１２４２９），国家自然科学基金（６０７０２０５９，６０９７２０７８），甘肃省自然科学基金（２００７ＧＳ０４８２３），网络安全与密码技术福建省高校重点实验室开放课题（０９Ａ００６）和兰州理工大学博士基金（ＢＳｌ４２００９０１）资助课题通信作者：张子彬ｚｚｂ０２