WAPI密钥管理协议的PCL证明

该文利用协议合成逻辑(PCL),对WAPI密钥管理协议进行了模块化正确性证明。首先,分析了相对独立的单播密钥协商与组播密钥通告协议,在满足一定的工作环境下,证明其分别具有SSA与KS特性,且与协议的实体与会话个数无关:接着,根据顺序合成规则与阶段合成定理,由于参与协议运行的实体避免了基于同一BK担当AE和ASUE两种角色,且每个子协议的运行都不干扰或不破坏其他子协议的环境条件,故WAPI密钥管理协议具有所需的安全属性,达到协议设计目标。