| WAPI密钥管理协议的PCL证明 |
| |
| 引用本文： | 铁满霞, 李建东, 王育民. WAPI密钥管理协议的PCL证明[J]. 电子与信息学报, 2009, 31(2): 444-447. doi: 10.3724/SP.J.1146.2007.01356 |
| |
| 作者姓名： | 铁满霞 李建东 王育民 |
| |
| 作者单位： | 西安电子科技大学ISN国家重点实验室,西安,710071;西安电子科技大学信息科学研究所,西安,710071 |
| |
| 基金项目： | 国家杰出青年科学基金，国家自然科学基金重大项目，国家高技术研究发展计划(863计划)，国家自然科学基金 |
| |
| 摘 要： | 该文利用协议合成逻辑(PCL)，对WAPI密钥管理协议进行了模块化正确性证明。首先，分析了相对独立的单播密钥协商与组播密钥通告协议，在满足一定的工作环境下，证明其分别具有SSA与KS特性，且与协议的实体与会话个数无关；接着，根据顺序合成规则与阶段合成定理，由于参与协议运行的实体避免了基于同一BK担当AE和ASUE两种角色，且每个子协议的运行都不干扰或不破坏其他子协议的环境条件，故WAPI密钥管理协议具有所需的安全属性，达到协议设计目标。
|
| 关 键 词： | 无线局域网 无线局域网鉴别与保密基础结构 密钥管理协议 协议合成逻辑 安全性证明 |
| 收稿时间： | 2007-08-23 |
| 修稿时间： | 2008-02-18 |
A Correctness Proof of WAPI Key Management Protocol Based on PCL |
| |
| Tie Man-xia, Li Jian-dong, Wang Yu-min. A Correctness Proof of WAPI Key Management Protocol Based on PCL[J]. Journal of Electronics & Information Technology, 2009, 31(2): 444-447. doi: 10.3724/SP.J.1146.2007.01356 |
| |
| Authors: | Tie Man-xia Li Jian-dong Wang Yu-min |
| |
| Affiliation: | State Key Laboratory of Integrated Services Networks;Xidian University;Xi'an 710071;China;Information Science Institute;China |
| |
| Abstract: | 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. |
| |
| Keywords: | WLAN WLAN Authentication and Privacy Infrastructure(WAPI) Key management protocol Protocol Composition Logic (PCL) Security proof |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《电子与信息学报》浏览原始摘要信息 |
|
点击此处可从《电子与信息学报》下载全文 |
