%0 Journal Article
%T A Correctness Proof of WAPI Key Management Protocol Based on PCL<br>WAPI密钥管理协议的PCL证明
%A Tie Man-xia
%A Li Jian-dong
%A Wang Yu-min
%A <br>铁满霞
%A 李建东
%A 王育民
%J 电子与信息学报
%D 2009
%I 
%X Based on PCL, a formal correctness proof of WAPI key management protocol is presented. First, unicast key negotiation and multicast key announcement sub-protocols are analyzed, and their separate proofs of specific security properties of SSA and KS are detailed under unbounded number of participants and sessions. Second, according to the sequential rule and staged composition theorem, all principals do not execute both roles of ASUE and AE, and the precondition of a sub-protocol is preserved by the other one later in the chain, so, WAPI key management protocol possesses the required security properties and achieves its predefined goals.
%K WLAN
%K WLAN Authentication and Privacy Infrastructure(WAPI)
%K Key management protocol
%K Protocol Composition Logic (PCL)
%K Security proof<br>无线局域网
%K 无线局域网鉴别与保密基础结构
%K 密钥管理协议
%K 协议合成逻辑
%K 安全性证明
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=1319827C0C74AAE8D654BEA21B7F54D3&jid=EFC0377B03BD8D0EF4BBB548AC5F739A&aid=8A30114EB85343B11DC39E35C4C98C05&yid=DE12191FBD62783C&vid=4AD960B5AD2D111A&iid=0B39A22176CE99FB&sid=68FDAD96FCC0AB1B&eid=C66DE7562B0326E2&journal_id=1009-5896&journal_name=电子与信息学报&referenced_num=0&reference_num=11