电子与信息学报
電子與信息學報
전자여신식학보
JOURNAL OF ELECTRONICS & INFORMATION TECHNOLOGY
2009年
2期
444-447
,共4页
无线局域网%无线局域网鉴别与保密基础结构%密钥管理协议%协议合成逻辑%安全性证明
無線跼域網%無線跼域網鑒彆與保密基礎結構%密鑰管理協議%協議閤成邏輯%安全性證明
무선국역망%무선국역망감별여보밀기출결구%밀약관리협의%협의합성라집%안전성증명
该文利用协议合成逻辑(PCL),对WAPI密钥管理协议进行了模块化正确性证明.首先,分析了相对独立的单播密钥协商与组播密钥通告协议,在满足一定的工作环境下,证明其分别具有SSA与KS特性,且与协议的实体与会话个数无关;接着,根据顺序合成规则与阶段合成定理,由于参与协议运行的实体避免了基于同一BK担当AE和ASUE两种角色,且每个子协议的运行都不干扰或不破坏其他子协议的环境条件,故WAPI密钥管理协议具有所需的安全属性,达到协议设计目标.
該文利用協議閤成邏輯(PCL),對WAPI密鑰管理協議進行瞭模塊化正確性證明.首先,分析瞭相對獨立的單播密鑰協商與組播密鑰通告協議,在滿足一定的工作環境下,證明其分彆具有SSA與KS特性,且與協議的實體與會話箇數無關;接著,根據順序閤成規則與階段閤成定理,由于參與協議運行的實體避免瞭基于同一BK擔噹AE和ASUE兩種角色,且每箇子協議的運行都不榦擾或不破壞其他子協議的環境條件,故WAPI密鑰管理協議具有所需的安全屬性,達到協議設計目標.
해문이용협의합성라집(PCL),대WAPI밀약관리협의진행료모괴화정학성증명.수선,분석료상대독립적단파밀약협상여조파밀약통고협의,재만족일정적공작배경하,증명기분별구유SSA여KS특성,차여협의적실체여회화개수무관;접착,근거순서합성규칙여계단합성정리,유우삼여협의운행적실체피면료기우동일BK담당AE화ASUE량충각색,차매개자협의적운행도불간우혹불파배기타자협의적배경조건,고WAPI밀약관리협의구유소수적안전속성,체도협의설계목표.
