WAPI密钥管理协议的PCL证明

vip

【文件原名】：WAPI密钥管理协议的PCL证明
【年份】：2009年
【语言】：中文
【页数】：4
【作者】：铁满霞[1,2] 李建东[1,2] 王育民[1,2]
[1]西安电子科技大学ISN国家重点实验室,西安710071 [2]西安电子科技大学信息科学研究所
【文件格式】：pdf
【摘要或目录】该文利用协议合成逻辑（PCL），对WAPI密钥管理协议进行了模块化正确性证明。首先，分析了相对独立的单播密钥协商与组播密钥通告协议，在满足一定的工作环境下，证明其分别具有SSA与KS特性，且与协议的实体与会话个数无关；接着，根据顺序合成规则与阶段合成定理，由于参与协议运行的实体避免了基于同一BK担当AE和ASUE两种角色，且每个子协议的运行都不干扰或不破坏其他子协议的环境条件，故WAPI密钥管理协议具有所需的安全属性，达到协议设计目标。
关 键 词:无线局域网 无线局域网鉴别与保密基础结构 密钥管理协议 协议合成逻辑 安全性证明